changeset 59621 | 291934bac95e |
parent 59573 | d09cc83cdce9 |
child 59917 | 9830c944670f |
--- a/src/Pure/simplifier.ML Fri Mar 06 14:01:08 2015 +0100 +++ b/src/Pure/simplifier.ML Fri Mar 06 15:58:56 2015 +0100 @@ -132,7 +132,7 @@ let val lhss' = prep lthy lhss; val ctxt' = fold Variable.auto_fixes lhss' lthy; - in Variable.export_terms ctxt' lthy lhss' end |> map (Proof_Context.cterm_of lthy), + in Variable.export_terms ctxt' lthy lhss' end |> map (Thm.cterm_of lthy), proc = proc, identifier = identifier}; in