--- 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;