changeset 41300 | 528f5d00b542 |
parent 41242 | 8edeb1dbbc76 |
child 41328 | 6792a5c92a58 |
--- a/src/HOL/Tools/SMT/smt_solver.ML Sun Dec 19 18:38:50 2010 -0800 +++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Dec 20 08:17:23 2010 +0100 @@ -214,10 +214,7 @@ int list * thm, default_max_relevant: int } -fun gen_solver_head ctxt iwthms = - SMT_Normalize.normalize ctxt iwthms - |> rpair ctxt - |-> SMT_Monomorph.monomorph +fun gen_solver_head ctxt iwthms = SMT_Normalize.normalize iwthms ctxt fun gen_solver_tail (name, info : solver_info) rm (iwthms', ctxt) iwthms = let