diff -r 7ecfa9beef91 -r c3ef007115a0 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 12:23:39 2010 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 13:19:31 2010 +0200
@@ -218,9 +218,8 @@
     lthy'
     |> Local_Theory.note (eq_abinding, [rec_rule])
     |-> (fn (_, rec') =>
-      Spec_Rules.add Spec_Rules.Equational ([f], [rec'])
-      |> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec'))
-    |> snd
+      Spec_Rules.add Spec_Rules.Equational ([f], rec')
+      #> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec') #> snd)
   end;
 
 val add_partial_function = gen_add_partial_function Specification.check_spec;