--- 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