# HG changeset patch
# User wenzelm
# Date 1160600117 -7200
# Node ID e4fd72aecd03346f3122ac950c5d1210411aa001
# Parent  7e5ba4a1f72f20befac7c246fe10825e02c42d30
add_defs: declare terms;

diff -r 7e5ba4a1f72f -r e4fd72aecd03 src/Pure/Isar/local_defs.ML
--- 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