add_defs: declare terms;

--- 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