diff -r 4a892432e8f1 -r afdc69f5156e src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Jan 12 23:29:03 2012 +0100
+++ b/src/HOL/Import/shuffler.ML	Fri Jan 13 11:50:28 2012 +0100
@@ -37,20 +37,6 @@
 
 val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context;
 
-fun mk_meta_eq th =
-    (case concl_of th of
-         Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th RS eq_reflection
-       | Const("==",_) $ _ $ _ => th
-       | _ => raise THM("Not an equality",0,[th]))
-    handle _ => raise THM("Couldn't make meta equality",0,[th])  (* FIXME avoid handle _ *)
-
-fun mk_obj_eq th =
-    (case concl_of th of
-         Const(@{const_name Trueprop},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _) => th
-       | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
-       | _ => raise THM("Not an equality",0,[th]))
-    handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
-
 structure ShuffleData = Theory_Data
 (
   type T = thm list
@@ -102,33 +88,6 @@
         Thm.equal_intr th1 th2 |> Drule.export_without_context
     end
 
-val def_norm =
-    let
-        val cert = cterm_of Pure.thy
-        val aT = TFree("'a",[])
-        val bT = TFree("'b",[])
-        val v = Free("v",aT)
-        val P = Free("P",aT-->bT)
-        val Q = Free("Q",aT-->bT)
-        val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
-        val cPQ = cert (Logic.mk_equals(P,Q))
-        val cv = cert v
-        val rew = Thm.assume cvPQ
-                         |> Thm.forall_elim cv
-                         |> Thm.abstract_rule "v" cv
-        val (lhs,rhs) = Logic.dest_equals(concl_of rew)
-        val th1 = Thm.transitive (Thm.transitive
-                                  (Thm.eta_conversion (cert lhs) |> Thm.symmetric)
-                                  rew)
-                             (Thm.eta_conversion (cert rhs))
-                             |> Thm.implies_intr cvPQ
-        val th2 = Thm.combination (Thm.assume cPQ) (Thm.reflexive cv)
-                              |> Thm.forall_intr cv
-                              |> Thm.implies_intr cPQ
-    in
-        Thm.equal_intr th1 th2 |> Drule.export_without_context
-    end
-
 val all_comm =
     let
         val cert = cterm_of Pure.thy
@@ -201,7 +160,7 @@
         all_comm RS init
     end
 
-fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
+fun quant_rewrite thy _ (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
     let
         val res = (find_bound 0 body;2) handle RESULT i => i
     in
@@ -270,7 +229,7 @@
     end
   | eta_redex _ = false
 
-fun eta_contract thy assumes origt =
+fun eta_contract thy _ origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
         val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
@@ -293,7 +252,7 @@
             end
     in
         case t of
-            Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
+            Const("all",_) $ (Abs(x,xT,Const("==",_) $ P $ Q)) =>
             (if eta_redex P andalso eta_redex Q
               then
                   let
@@ -314,7 +273,6 @@
                                      |> Thm.implies_intr cu
                       val rew_th = Thm.equal_intr (th' |> Thm.implies_intr ct) uth'
                       val res = final rew_th
-                      val lhs = (#1 (Logic.dest_equals (prop_of res)))
                   in
                        SOME res
                   end
@@ -322,17 +280,7 @@
           | _ => NONE
        end
 
-fun beta_fun thy assume t =
-    SOME (Thm.beta_conversion true (cterm_of thy t))
-
-val meta_sym_rew = @{thm refl}
-
-fun equals_fun thy assume t =
-    case t of
-        Const("op ==",_) $ u $ v => if Term_Ord.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
-      | _ => NONE
-
-fun eta_expand thy assumes origt =
+fun eta_expand thy _ origt =
     let
         val (typet,Tinst) = freeze_thaw_term origt
         val (init,thaw) = Drule.legacy_freeze_thaw (Thm.reflexive (cterm_of thy typet))
@@ -400,17 +348,6 @@
 val S  = mk_free "S" xT
 val S'  = mk_free "S'" xT
 in
-fun beta_simproc thy = Simplifier.simproc_global_i
-                      thy
-                      "Beta-contraction"
-                      [Abs("x",xT,Q) $ S]
-                      beta_fun
-
-fun equals_simproc thy = Simplifier.simproc_global_i
-                      thy
-                      "Ordered rewriting of meta equalities"
-                      [Const("op ==",xT) $ S $ S']
-                      equals_fun
 
 fun quant_simproc thy = Simplifier.simproc_global_i
                            thy
@@ -564,7 +501,6 @@
         val rew_th = norm_term thy closed_t
         val rhs = Thm.rhs_of rew_th
 
-        val shuffles = ShuffleData.get thy
         fun process [] = NONE
           | process ((name,th)::thms) =
             let