Element.generalize_facts;

--- a/src/Pure/Tools/invoke.ML	Wed Nov 29 04:11:16 2006 +0100
+++ b/src/Pure/Tools/invoke.ML	Wed Nov 29 04:11:17 2006 +0100
@@ -74,7 +74,7 @@
           val notes =
             maps (Element.facts_of thy) elems'
             |> Element.satisfy_facts prems''
-            |> Element.export_facts ctxt'' ctxt
+            |> Element.generalize_facts ctxt'' ctxt
             |> Attrib.map_facts (Attrib.attribute_i thy)
             |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));
         in