# HG changeset patch
# User wenzelm
# Date 1164769877 -3600
# Node ID 22c9392de970d22effa042db72eee002dc65cbb1
# Parent  6fb553dc039b7ca775d3169b9a4b226de2579fc1
Element.generalize_facts;

diff -r 6fb553dc039b -r 22c9392de970 src/Pure/Tools/invoke.ML
--- 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