src/ZF/Tools/typechk.ML
changeset 35409 5c5bb83f2bae
parent 33519 e31a85f92ce9
child 36960 01594f816e3a
     1.1 --- a/src/ZF/Tools/typechk.ML	Sat Feb 27 23:13:01 2010 +0100
     1.2 +++ b/src/ZF/Tools/typechk.ML	Sun Feb 28 22:30:51 2010 +0100
     1.3 @@ -98,7 +98,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 FalseE 1
     1.8 +    (DEPTH_SOLVE (etac @{thm 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))));