src/Pure/Isar/overloading.ML

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