# HG changeset patch
# User wenzelm
# Date 1144922461 -7200
# Node ID 51eeee99bd8fd0ec03e0725538ae641450d31e9e
# Parent  bba26da0f22754a9d48d816fc1ed243f1bfafc22
use conjunction stuff from conjunction.ML;

diff -r bba26da0f227 -r 51eeee99bd8f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Apr 13 12:01:01 2006 +0200
@@ -1620,12 +1620,12 @@
     val intro = Drule.standard (Goal.prove defs_thy [] norm_ts statement (fn _ =>
       Tactic.rewrite_goals_tac [pred_def] THEN
       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
-      Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
+      Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
 
     val conjuncts =
-      (Drule.equal_elim_rule1 OF [Thm.symmetric body_eq,
+      (Drule.equal_elim_rule2 OF [body_eq,
         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
-      |> Drule.conj_elim_precise [length ts] |> hd;
+      |> Conjunction.elim_precise [length ts] |> hd;
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       prove_protected defs_thy t
        (Tactic.rewrite_goals_tac defs THEN
diff -r bba26da0f227 -r 51eeee99bd8f src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Apr 13 12:01:01 2006 +0200
@@ -496,7 +496,7 @@
     val _ = conditional (not (Pattern.matches thy
         (Logic.mk_conjunction_list2 propss, Thm.prop_of th))) (fn () =>
       error ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th));
-  in Drule.conj_elim_precise (map length propss) th end;
+  in Conjunction.elim_precise (map length propss) th end;
 
 
 
diff -r bba26da0f227 -r 51eeee99bd8f src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Thu Apr 13 12:01:01 2006 +0200
@@ -195,7 +195,7 @@
   if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   else
     Drule.fconv_rule
-      (Drule.concl_conv ~1 (Drule.conjunction_conv ~1
+      (Drule.concl_conv ~1 (Conjunction.conv ~1
         (K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th;
 
 in
@@ -337,7 +337,7 @@
         else
           SOME (ns,
             ths
-            |> foldr1 (uncurry Drule.conj_intr)
+            |> foldr1 (uncurry Conjunction.intr)
             |> Drule.implies_intr_list prems
             |> Drule.standard'
             |> save (hd raw_rules)
diff -r bba26da0f227 -r 51eeee99bd8f src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/goal.ML	Thu Apr 13 12:01:01 2006 +0200
@@ -147,7 +147,7 @@
     val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
       err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
   in
-    hd (Drule.conj_elim_precise [length props] raw_result)
+    hd (Conjunction.elim_precise [length props] raw_result)
     |> map
       (Drule.implies_intr_list casms
         #> Drule.forall_intr_list cparams
@@ -176,12 +176,12 @@
 fun extract i n st =
   (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
    else if n = 1 then Seq.single (Thm.cprem_of st i)
-   else Seq.single (foldr1 Drule.mk_conjunction (map (Thm.cprem_of st) (i upto (i + n - 1)))))
+   else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
   |> Seq.map (Thm.adjust_maxidx #> init);
 
 fun retrofit i n st' st =
   (if n = 1 then st
-   else st |> Drule.rotate_prems (i - 1) |> Drule.conj_uncurry n |> Drule.rotate_prems (1 - i))
+   else st |> Drule.rotate_prems (i - 1) |> Conjunction.uncurry n |> Drule.rotate_prems (1 - i))
   |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
 
 fun SELECT_GOAL tac i st =
diff -r bba26da0f227 -r 51eeee99bd8f src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Apr 13 12:01:00 2006 +0200
+++ b/src/Pure/tactic.ML	Thu Apr 13 12:01:01 2006 +0200
@@ -642,7 +642,7 @@
 (* meta-level conjunction *)
 
 val conj_tac = SUBGOAL (fn (goal, i) =>
-  if can Logic.dest_conjunction goal then rtac Drule.conjunctionI i
+  if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
   else no_tac);
 
 val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
@@ -657,12 +657,12 @@
 fun CONJUNCTS tac =
   SELECT_GOAL (conjunction_tac 1
     THEN tac
-    THEN PRIMITIVE (Drule.conj_uncurry ~1));
+    THEN PRIMITIVE (Conjunction.uncurry ~1));
 
 fun PRECISE_CONJUNCTS n tac =
   SELECT_GOAL (precise_conjunction_tac n 1
     THEN tac
-    THEN PRIMITIVE (Drule.conj_uncurry ~1));
+    THEN PRIMITIVE (Conjunction.uncurry ~1));
 
 end;