# HG changeset patch
# User krauss
# Date 1288091971 -7200
# Node ID c3ef007115a084f9afe35dea0e7c15f2646a243d
# Parent  7ecfa9beef91588074c2cefb476b9d5c352a96a3
fixed confusion introduced in 008dc2d2c395

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;