Element.export_facts;

--- a/src/Pure/Tools/invoke.ML	Sat Oct 07 01:31:20 2006 +0200
+++ b/src/Pure/Tools/invoke.ML	Sat Oct 07 01:31:22 2006 +0200
@@ -73,7 +73,7 @@
           val notes =
             maps (Element.facts_of thy) elems'
             |> Element.satisfy_facts prems''
-            |> Element.generalize_facts ctxt'' ctxt
+            |> Element.export_facts ctxt'' ctxt
             |> Attrib.map_facts (Attrib.attribute_i thy)
             |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));
         in