# HG changeset patch
# User wenzelm
# Date 1160177482 -7200
# Node ID c99f79910ae83d4c9bdbe08e50fd4b797b6d1c79
# Parent  318f0ff93d994931b737f84375e006b7caccc0b5
Element.export_facts;

diff -r 318f0ff93d99 -r c99f79910ae8 src/Pure/Tools/invoke.ML
--- 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