# HG changeset patch
# User wenzelm
# Date 1183475829 -7200
# Node ID 58147e5bd070f6a10c81e237a2f22ae50928faf0
# Parent  3f82d17989762ddbf81c14bfead32e4020635412
removed obsolete mk_conjunction_list, intr/elim_list;

diff -r 3f82d1798976 -r 58147e5bd070 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Tue Jul 03 17:17:09 2007 +0200
+++ b/src/Pure/conjunction.ML	Tue Jul 03 17:17:09 2007 +0200
@@ -9,7 +9,6 @@
 sig
   val conjunction: cterm
   val mk_conjunction: cterm * cterm -> cterm
-  val mk_conjunction_list: cterm list -> cterm
   val mk_conjunction_balanced: cterm list -> cterm
   val dest_conjunction: cterm -> cterm * cterm
   val cong: thm -> thm -> thm
@@ -18,10 +17,8 @@
   val conjunctionD2: thm
   val conjunctionI: thm
   val intr: thm -> thm -> thm
-  val intr_list: thm list -> thm
   val intr_balanced: thm list -> thm
   val elim: thm -> thm * thm
-  val elim_list: thm -> thm list
   val elim_balanced: int -> thm -> thm list
   val curry_balanced: int -> thm -> thm
   val uncurry_balanced: int -> thm -> thm
@@ -40,9 +37,6 @@
 
 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
 
-fun mk_conjunction_list [] = true_prop
-  | mk_conjunction_list ts = foldr1 mk_conjunction ts;
-
 fun mk_conjunction_balanced [] = true_prop
   | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
 
@@ -114,18 +108,11 @@
 end;
 
 
-(* multiple conjuncts *)
-
-fun intr_list [] = asm_rl
-  | intr_list ths = foldr1 (uncurry intr) ths;
+(* balanced conjuncts *)
 
 fun intr_balanced [] = asm_rl
   | intr_balanced ths = BalancedTree.make (uncurry intr) ths;
 
-fun elim_list th =   (* FIXME improper!? rename to "elims" *)
-  let val (th1, th2) = elim th
-  in elim_list th1 @ elim_list th2 end handle THM _ => [th];
-
 fun elim_balanced 0 _ = []
   | elim_balanced n th = BalancedTree.dest elim n th;