--- a/src/Pure/Isar/class.ML Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/class.ML Thu Aug 26 15:48:08 2010 +0200
@@ -482,7 +482,7 @@
val type_name = sanitize_name o Long_Name.base_name;
-fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result
+fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result
(AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
##> Local_Theory.target synchronize_inst_syntax;
@@ -572,7 +572,7 @@
val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
fun after_qed' results =
- Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
+ Local_Theory.background_theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
#> after_qed;
in
lthy