# 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;