--- a/src/Pure/conjunction.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/Pure/conjunction.ML Tue Apr 15 16:12:05 2008 +0200
@@ -74,7 +74,7 @@
fun conjunctionD which =
Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
- Drule.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
+ Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
in
@@ -130,7 +130,7 @@
fun comp_rule th rule =
Thm.adjust_maxidx_thm ~1 (th COMP
- (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
+ (rule |> Drule.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
in