# HG changeset patch
# User wenzelm
# Date 1333215521 -7200
# Node ID 72ab1fbf2f41097cd52df9084705a2d54108fc07
# Parent  0b1829860149a48b9150035ca8f232961fff6443
tuned;

diff -r 0b1829860149 -r 72ab1fbf2f41 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sat Mar 31 19:26:23 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sat Mar 31 19:38:41 2012 +0200
@@ -82,12 +82,12 @@
     (*local definition*)
     val ((lhs, local_def), lthy3) = lthy2
       |> Local_Defs.add_def ((b, NoSyn), lhs');
-    val def' = Thm.transitive local_def global_def;
+
+    (*result*)
     val def =
-      Local_Defs.contract defs
-        (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs))) def';
-
-    (*note*)
+      Thm.transitive local_def global_def
+      |> Local_Defs.contract defs
+          (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs)));
     val ([(res_name, [res])], lthy4) = lthy3
       |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
   in ((lhs, (res_name, res)), lthy4) end;