1.1 --- a/src/Pure/Isar/overloading.ML	Thu Aug 26 13:09:12 2010 +0200
     1.2 +++ b/src/Pure/Isar/overloading.ML	Thu Aug 26 15:48:08 2010 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4    end
     1.5  
     1.6  fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
     1.7 -  Local_Theory.theory_result
     1.8 +  Local_Theory.background_theory_result
     1.9      (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
    1.10    ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
    1.11    ##> Local_Theory.target synchronize_syntax