diff -r 19eefc0655b6 -r cfde251d03a5 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Thu Mar 11 23:47:16 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Fri Mar 12 12:14:30 2010 +0100
@@ -130,8 +130,9 @@
     fun define_overloaded (def_name, eq) lthy =
       let
         val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
-        val ((_, (_, thm)), lthy') = lthy
-          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
+        val (thm, lthy') = lthy
+          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
+          |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;