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