# HG changeset patch
# User wenzelm
# Date 1154287739 -7200
# Node ID 6fb7347898184926c0f65ae10e24df467c89016d
# Parent  219a996d8bde147dce85b42bae6c2bb2791e9ba8
proper Element.generalize_facts;

diff -r 219a996d8bde -r 6fb734789818 src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Sun Jul 30 21:28:58 2006 +0200
+++ b/src/Pure/Tools/invoke.ML	Sun Jul 30 21:28:59 2006 +0200
@@ -70,20 +70,17 @@
           val elems' = elems |> map (Element.inst_ctxt thy
             (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
           val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
-
-          val Element.Notes notes = 
-            Element.Notes (maps (Element.facts_of thy) elems')
-            |> Element.satisfy_ctxt prems''
-            |> Element.map_ctxt_values I I (singleton (ProofContext.export ctxt'' ctxt));
-            (* FIXME export typs/terms *)
-          val notes' = notes
+          val notes =
+            maps (Element.facts_of thy) elems'
+            |> Element.satisfy_facts prems''
+            |> Element.generalize_facts ctxt'' ctxt
             |> Attrib.map_facts (Attrib.attribute_i thy)
-            |> map (fn ((a, atts), facts) => ((a, atts @ more_atts), facts));
+            |> map (fn ((a, atts), bs) => ((a, atts @ more_atts), bs));
         in
           ctxt
           |> ProofContext.sticky_prefix prfx
           |> ProofContext.qualified_names
-          |> (snd o ProofContext.note_thmss_i notes')
+          |> (snd o ProofContext.note_thmss_i notes)
           |> ProofContext.restore_naming ctxt
         end) #> Proof.put_facts NONE);
   in