# 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