diff -r 42c37cf849cd -r 19deea200358 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -165,8 +165,9 @@
 
 fun declare c_ty = pair (Const c_ty);
 
-fun define checked b (c, t) = Thm.add_def (not checked) true
-  (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
+fun define checked b (c, t) =
+  Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
+  #>> snd;
 
 fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
   #> Local_Theory.target synchronize_syntax