diff -r e84d900cd287 -r 59203adfc33f src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Thu Oct 30 16:20:46 2014 +0100
+++ b/src/ZF/Tools/typechk.ML	Thu Oct 30 16:55:29 2014 +0100
@@ -99,7 +99,7 @@
 (*Instantiates variables in typing conditions.
   drawback: does not simplify conjunctions*)
 fun type_solver_tac ctxt hyps = SELECT_GOAL
-    (DEPTH_SOLVE (etac @{thm FalseE} 1
+    (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
                   ORELSE basic_res_tac 1
                   ORELSE (ares_tac hyps 1
                           APPEND typecheck_step_tac (tcset_of ctxt))));