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