changeset 20243 | 8b64a1ea9b1b |
parent 20236 | 54e15870444b |
child 20252 | bad805d0456b |
--- a/src/Pure/Isar/local_theory.ML Thu Jul 27 23:28:27 2006 +0200 +++ b/src/Pure/Isar/local_theory.ML Thu Jul 27 23:28:28 2006 +0200 @@ -249,7 +249,7 @@ in fun axioms_finish finish = fold_map (fn ((name, atts), props) => - fold ProofContext.fix_frees props + fold Variable.fix_frees props #> (fn ctxt => ctxt |> theory_result (fold_map (add_axiom (hyps_of ctxt)) (PureThy.name_multi name props)) |-> (fn ths => note ((name, atts), map (finish ctxt) ths))));