changeset 58838 | 59203adfc33f |
parent 58828 | 6d076fdd933d |
child 58893 | 9e0ecb66d6a7 |
--- 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))));