# HG changeset patch
# User wenzelm
# Date 1333213799 -7200
# Node ID 289dcbdd59849ba162bee9314a2a1044fd519bc8
# Parent  b61a11dea74c690391a7bd96f773a4c4f3780819
more direct Local_Defs.contract;
eliminated slightly odd Local_Defs.trans_term/trans_prop;

diff -r b61a11dea74c -r 289dcbdd5984 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sat Mar 31 15:29:49 2012 +0200
+++ b/src/HOL/Tools/typedef.ML	Sat Mar 31 19:09:59 2012 +0200
@@ -192,7 +192,7 @@
 
         val cert = Thm.cterm_of (Proof_Context.theory_of axiom_lthy);
         val typedef =
-          Local_Defs.contract axiom_lthy defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom;
+          Local_Defs.contract defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom;
       in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end;
 
     val alias_lthy = typedef_lthy
@@ -210,7 +210,7 @@
       let
         val cert = Thm.cterm_of (Proof_Context.theory_of lthy1);
         val inhabited' =
-          Local_Defs.contract lthy1 (the_list set_def) (cert (mk_inhabited set')) inhabited;
+          Local_Defs.contract (the_list set_def) (cert (mk_inhabited set')) inhabited;
         val typedef' = inhabited' RS typedef;
         fun make th = Goal.norm_result (typedef' RS th);
         val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
diff -r b61a11dea74c -r 289dcbdd5984 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sat Mar 31 15:29:49 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sat Mar 31 19:09:59 2012 +0200
@@ -58,7 +58,6 @@
     (*term and type parameters*)
     val crhs = Thm.cterm_of thy rhs;
     val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
-    val rhs_conv = Raw_Simplifier.rewrite true defs crhs;
 
     val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
     val T = Term.fastype_of rhs;
@@ -83,10 +82,10 @@
     (*local definition*)
     val ((lhs, local_def), lthy3) = lthy2
       |> Local_Defs.add_def ((b, NoSyn), lhs');
-    val def = Local_Defs.trans_terms lthy3
-      [(*c == global.c xs*)     local_def,
-       (*global.c xs == rhs'*)  global_def,
-       (*rhs' == rhs*)          Thm.symmetric rhs_conv];
+    val def' = Thm.transitive local_def global_def;
+    val def =
+      Local_Defs.contract defs
+        (Thm.cterm_of (Proof_Context.theory_of lthy3) (Logic.mk_equals (lhs, rhs))) def';
 
     (*note*)
     val ([(res_name, [res])], lthy4) = lthy3
@@ -134,7 +133,7 @@
     val result'' =
       (fold (curry op COMP) asms' result'
         handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
-      |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
+      |> Local_Defs.contract defs (Thm.cprop_of th)
       |> Goal.norm_result
       |> Global_Theory.name_thm false false name;
 
diff -r b61a11dea74c -r 289dcbdd5984 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Mar 31 15:29:49 2012 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sat Mar 31 19:09:59 2012 +0200
@@ -17,9 +17,7 @@
     (term * term) * Proof.context
   val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm
   val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm
-  val trans_terms: Proof.context -> thm list -> thm
-  val trans_props: Proof.context -> thm list -> thm
-  val contract: Proof.context -> thm list -> cterm -> thm -> thm
+  val contract: thm list -> cterm -> thm -> thm
   val print_rules: Proof.context -> unit
   val defn_add: attribute
   val defn_del: attribute
@@ -166,30 +164,8 @@
 fun export_cterm inner outer ct =
   export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
 
-
-(* basic transitivity reasoning -- modulo beta-eta *)
-
-local
-
-val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of;
-
-fun trans_list _ _ [] = raise List.Empty
-  | trans_list trans ctxt (th :: raw_eqs) =
-      (case filter_out is_trivial raw_eqs of
-        [] => th
-      | eqs =>
-          let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
-          in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);
-
-in
-
-val trans_terms = trans_list (fn eq2 => fn eq1 => eq2 COMP (eq1 COMP Drule.transitive_thm));
-val trans_props = trans_list (fn eq => fn th => th COMP (eq COMP Drule.equal_elim_rule1));
-
-end;
-
-fun contract ctxt defs ct th =
-  trans_props ctxt [th, Thm.symmetric (Raw_Simplifier.rewrite true defs ct)];
+fun contract defs ct th =
+  th COMP (Raw_Simplifier.rewrite true defs ct COMP_INCR Drule.equal_elim_rule2);