# HG changeset patch # User haftmann # Date 1150791382 -7200 # Node ID 5c882c3e610b15eeadfcf7cb102484811ea98f5a # Parent cb8472f4c5fd5351c3537ad0b703ee84b29a57cb switched to open locales for classes diff -r cb8472f4c5fd -r 5c882c3e610b src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Tue Jun 20 10:10:06 2006 +0200 +++ b/src/Pure/Tools/class_package.ML Tue Jun 20 10:16:22 2006 +0200 @@ -398,7 +398,7 @@ #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, mapp_this)) #> prove_interpretation_i (NameSpace.base name_locale, []) (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this))) - ((ALLGOALS o resolve_tac) ax_axioms) + ((ALLGOALS o ProofContext.fact_tac) ax_axioms) #> pair ctxt ))))) end;