# HG changeset patch
# User wenzelm
# Date 1158055959 -7200
# Node ID 8182d961c7cc6c7c2f93b4590b28781c11fea005
# Parent  bb68343f6f83e3af91e43508adb01b76ef49b0cf
intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;

diff -r bb68343f6f83 -r 8182d961c7cc src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Tue Sep 12 12:12:33 2006 +0200
+++ b/src/Pure/conjunction.ML	Tue Sep 12 12:12:39 2006 +0200
@@ -74,8 +74,8 @@
 
 local
 
-val A = read "PROP A";
-val B = read "PROP B";
+val A = read "PROP A" and vA = read "PROP ?A";
+val B = read "PROP B" and vB = read "PROP ?B";
 val C = read "PROP C";
 val ABC = read "PROP A ==> PROP B ==> PROP C";
 val A_B = read "PROP ProtoPure.conjunction(A, B)"
@@ -98,14 +98,25 @@
       (Thm.forall_intr C (Thm.implies_intr ABC
         (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
 
-fun intr tha thb = thb COMP (tha COMP Drule.incr_indexes2 tha thb conjunctionI);
+fun intr tha thb =
+  Thm.implies_elim
+    (Thm.implies_elim
+      (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
+    tha)
+  thb;
 
 fun intr_list [] = asm_rl
   | intr_list ths = foldr1 (uncurry intr) ths;
 
 fun elim th =
- (th COMP Drule.incr_indexes th conjunctionD1,
-  th COMP Drule.incr_indexes th conjunctionD2);
+  let
+    val (A, B) = dest_conjunction (Thm.cprop_of th)
+      handle TERM (msg, _) => raise THM (msg, 0, [th]);
+    val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
+  in
+   (Thm.implies_elim (inst conjunctionD1) th,
+    Thm.implies_elim (inst conjunctionD2) th)
+  end;
 
 (*((A && B) && C) && D && E -- flat*)
 fun elim_list th =