src/ZF/Tools/typechk.ML

                                      @{thm ballI}, @{thm allI}, @{thm conjI}, @{thm impI}];
 
 (*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))));
 
 val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss =>