src/ZF/Tools/typechk.ML

--- a/src/ZF/Tools/typechk.ML	Sat Feb 27 23:13:01 2010 +0100
+++ b/src/ZF/Tools/typechk.ML	Sun Feb 28 22:30:51 2010 +0100
@@ -98,7 +98,7 @@
 (*Instantiates variables in typing conditions.
   drawback: does not simplify conjunctions*)
 fun type_solver_tac ctxt hyps = SELECT_GOAL
-    (DEPTH_SOLVE (etac FalseE 1
+    (DEPTH_SOLVE (etac @{thm FalseE} 1
                   ORELSE basic_res_tac 1
                   ORELSE (ares_tac hyps 1
                           APPEND typecheck_step_tac (tcset_of ctxt))));