1.1 --- a/src/Pure/drule.ML	Mon Jun 25 17:44:16 2012 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Jun 25 17:50:05 2012 +0200
     1.3 @@ -105,7 +105,6 @@
     1.4    val incr_indexes2: thm -> thm -> thm -> thm
     1.5    val triv_forall_equality: thm
     1.6    val distinct_prems_rl: thm
     1.7 -  val swap_prems_rl: thm
     1.8    val equal_intr_rule: thm
     1.9    val equal_elim_rule1: thm
    1.10    val equal_elim_rule2: thm
    1.11 @@ -565,24 +564,6 @@
    1.12        (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
    1.13    end;
    1.14  
    1.15 -(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
    1.16 -   (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
    1.17 -   `thm COMP swap_prems_rl' swaps the first two premises of `thm'
    1.18 -*)
    1.19 -val swap_prems_rl =
    1.20 -  let
    1.21 -    val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
    1.22 -    val major = Thm.assume cmajor;
    1.23 -    val cminor1 = read_prop "PhiA";
    1.24 -    val minor1 = Thm.assume cminor1;
    1.25 -    val cminor2 = read_prop "PhiB";
    1.26 -    val minor2 = Thm.assume cminor2;
    1.27 -  in
    1.28 -    store_standard_thm_open (Binding.name "swap_prems_rl")
    1.29 -      (Thm.implies_intr cmajor (Thm.implies_intr cminor2 (Thm.implies_intr cminor1
    1.30 -        (Thm.implies_elim (Thm.implies_elim major minor1) minor2))))
    1.31 -  end;
    1.32 -
    1.33  (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
    1.34     ==> PROP ?phi == PROP ?psi
    1.35     Introduction rule for == as a meta-theorem.