# HG changeset patch
# User wenzelm
# Date 1340639405 -7200
# Node ID d30957198bbb9cf96d720adf1c69fc475f930e20
# Parent  cdbdbfa6a29fde4b65264865fd392d4ff282efde
eliminated obsolete swap_prems_rl -- rotate_prems usually does the job more directly;

diff -r cdbdbfa6a29f -r d30957198bbb src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Jun 25 17:44:16 2012 +0200
+++ b/src/Pure/drule.ML	Mon Jun 25 17:50:05 2012 +0200
@@ -105,7 +105,6 @@
   val incr_indexes2: thm -> thm -> thm -> thm
   val triv_forall_equality: thm
   val distinct_prems_rl: thm
-  val swap_prems_rl: thm
   val equal_intr_rule: thm
   val equal_elim_rule1: thm
   val equal_elim_rule2: thm
@@ -565,24 +564,6 @@
       (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
   end;
 
-(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
-   (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
-   `thm COMP swap_prems_rl' swaps the first two premises of `thm'
-*)
-val swap_prems_rl =
-  let
-    val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
-    val major = Thm.assume cmajor;
-    val cminor1 = read_prop "PhiA";
-    val minor1 = Thm.assume cminor1;
-    val cminor2 = read_prop "PhiB";
-    val minor2 = Thm.assume cminor2;
-  in
-    store_standard_thm_open (Binding.name "swap_prems_rl")
-      (Thm.implies_intr cmajor (Thm.implies_intr cminor2 (Thm.implies_intr cminor1
-        (Thm.implies_elim (Thm.implies_elim major minor1) minor2))))
-  end;
-
 (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
    ==> PROP ?phi == PROP ?psi
    Introduction rule for == as a meta-theorem.