add_defs: declare terms;
authorwenzelm
Wed Oct 11 22:55:17 2006 +0200 (2006-10-11)
changeset 20980e4fd72aecd03
parent 20979 7e5ba4a1f72f
child 20981 c4d3fc6e1e64
add_defs: declare terms;
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Wed Oct 11 22:55:16 2006 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Oct 11 22:55:17 2006 +0200
     1.3 @@ -96,6 +96,7 @@
     1.4    in
     1.5      ctxt
     1.6      |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
     1.7 +    |> fold Variable.declare_term eqs
     1.8      |> ProofContext.add_assms_i def_export
     1.9        (map2 (fn a => fn eq => (a, [(eq, [])])) (names' ~~ atts) eqs)
    1.10      |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss