src/ZF/Tools/typechk.ML
changeset 58838 59203adfc33f
parent 58828 6d076fdd933d
child 58893 9e0ecb66d6a7
     1.1 --- a/src/ZF/Tools/typechk.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/ZF/Tools/typechk.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4  (*Instantiates variables in typing conditions.
     1.5    drawback: does not simplify conjunctions*)
     1.6  fun type_solver_tac ctxt hyps = SELECT_GOAL
     1.7 -    (DEPTH_SOLVE (etac @{thm FalseE} 1
     1.8 +    (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
     1.9                    ORELSE basic_res_tac 1
    1.10                    ORELSE (ares_tac hyps 1
    1.11                            APPEND typecheck_step_tac (tcset_of ctxt))));