--- a/src/Pure/drule.ML Tue Jan 15 00:08:51 2002 +0100
+++ b/src/Pure/drule.ML Tue Jan 15 00:09:29 2002 +0100
@@ -923,7 +923,9 @@
in
fun conj_intr tha thb = thb COMP (tha COMP incr [tha, thb] conj_intr_rule);
-val conj_intr_list = foldr1 (uncurry conj_intr);
+
+fun conj_intr_list [] = asm_rl
+ | conj_intr_list ths = foldr1 (uncurry conj_intr) ths;
fun conj_elim th =
let val th' = forall_elim_var (#maxidx (Thm.rep_thm th) + 1) th
@@ -933,7 +935,8 @@
let val (th1, th2) = conj_elim th
in conj_elim_list th1 @ conj_elim_list th2 end handle THM _ => [th];
-fun conj_elim_precise 1 th = [th]
+fun conj_elim_precise 0 _ = []
+ | conj_elim_precise 1 th = [th]
| conj_elim_precise n th =
let val (th1, th2) = conj_elim th
in th1 :: conj_elim_precise (n - 1) th2 end;