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