Merge pull request #1276 from CakeML/checkthm_fastbuild

Author: myreen

.gitignore

@@ -7,6 +7,8 @@
 *.ui
 *.o
 .hol
+.HOLMK
+.hollogs
 
 # TacticToe
 *Script_ttt.sml

misc/preamble.sml

@@ -47,7 +47,11 @@ fun impl_subgoal_tac th =
 (* -- *)
 
 fun check_tag t = Tag.isEmpty t orelse Tag.isDisk t
-val check_thm = Lib.assert (check_tag o Thm.tag)
+fun check_thm t = (
+  prove(T, fn g => (
+    (if check_tag (Thm.tag t) then () else failwith "theorem depends on cheats");
+    ACCEPT_TAC TRUTH g));
+  t)
 
 val option_bind_tm = prim_mk_const{Thy="option",Name="OPTION_BIND"};
 val option_ignore_bind_tm = prim_mk_const{Thy="option",Name="OPTION_IGNORE_BIND"};