src/Pure/Isar/local_defs.ML

   val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
     (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
   val meta_rewrite_conv: Proof.context -> conv
   val meta_rewrite_rule: Proof.context -> thm -> thm

      TERM b as          b xs == b as
 *)
 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);
 
 
 
 (** defived definitions **)