changeset 39288 | f1ae2493d93f |
parent 39134 | 917b4b6ba3d2 |
child 39353 | 7f11d833d65b |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Sep 12 17:39:02 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Sep 12 19:04:02 2010 +0200 @@ -437,7 +437,7 @@ in repair_tvar_sorts (do_formula true phi Vartab.empty) end fun check_formula ctxt = - Type_Infer.constrain HOLogic.boolT + Type.constraint HOLogic.boolT #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)