changeset 20980 | e4fd72aecd03 |
parent 20909 | 7132ab2b4621 |
child 21506 | b2a673894ce5 |
--- a/src/Pure/Isar/local_defs.ML Wed Oct 11 22:55:16 2006 +0200 +++ b/src/Pure/Isar/local_defs.ML Wed Oct 11 22:55:17 2006 +0200 @@ -96,6 +96,7 @@ in ctxt |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2 + |> fold Variable.declare_term eqs |> ProofContext.add_assms_i def_export (map2 (fn a => fn eq => (a, [(eq, [])])) (names' ~~ atts) eqs) |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss