# HG changeset patch
# User wenzelm
# Date 1166106682 -3600
# Node ID da545169fe06e965a1bdb7cb6e4196a8931e929d
# Parent  e10b8bd7a886f60613b87ae33193c96f6f49911e
defs/notes: more robust transitivity reasoning;

diff -r e10b8bd7a886 -r da545169fe06 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Dec 14 15:31:21 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Dec 14 15:31:22 2006 +0100
@@ -121,12 +121,9 @@
 
 (* defs *)
 
-local
+
 
-infix also;
-
-fun eq1 also eq2 =
-  eq2 COMP (eq1 COMP (Drule.incr_indexes2 eq1 eq2 transitive_thm));
+local
 
 fun expand_term ctxt t =
   let
@@ -157,10 +154,10 @@
         val (def, lthy3) = lthy2
           |> LocalTheory.theory_result (add_def (name', Logic.mk_equals (lhs', rhs')));
 
-        val eq =
-          (*c == loc.c xs*) lhs_def
-          (*lhs' == rhs'*)  also def
-          (*rhs' == rhs*)   also Thm.symmetric rhs_conv;
+        val eq = LocalDefs.trans_terms lthy3
+          [(*c == loc.c xs*) lhs_def,
+           (*lhs' == rhs'*)  def,
+           (*rhs' == rhs*)   Thm.symmetric rhs_conv];
       in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
 
     val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
@@ -246,7 +243,7 @@
     val result'' =
       (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
         NONE => raise THM ("Failed to re-import result", 0, [result'])
-      | SOME res => res) COMP (concl_conv COMP_INCR Drule.equal_elim_rule2)
+      | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
       |> Goal.norm_result
       |> PureThy.name_thm false false name;