# HG changeset patch
# User wenzelm
# Date 1329334099 -3600
# Node ID 2accd201e5bc10029c99bbf319974eca27f294ad
# Parent  994302b6f32e6bbfff95356b6d96b72a71e6bf60
removed dead code;

diff -r 994302b6f32e -r 2accd201e5bc src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Wed Feb 15 20:24:21 2012 +0100
+++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Feb 15 20:28:19 2012 +0100
@@ -6,18 +6,13 @@
 
 signature CASE_SPLIT =
 sig
-
   (* try to recursively split conjectured thm to given list of thms *)
   val splitto : thm list -> thm -> thm
-
 end;
 
 structure CaseSplit: CASE_SPLIT =
 struct
 
-val rulify_goals = Raw_Simplifier.rewrite_goals_rule @{thms induct_rulify};
-val atomize_goals = Raw_Simplifier.rewrite_goals_rule @{thms induct_atomize};
-
 (* beta-eta contract the theorem *)
 fun beta_eta_contract thm =
     let
@@ -56,9 +51,6 @@
       val abs_ct = ctermify abst;
       val free_ct = ctermify x;
 
-      val casethm_vars = rev (Misc_Legacy.term_vars (Thm.concl_of case_thm));
-
-      val casethm_tvars = Misc_Legacy.term_tvars (Thm.concl_of case_thm);
       val (Pv, Dv, type_insts) =
           case (Thm.concl_of case_thm) of
             (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) =>
@@ -102,7 +94,7 @@
     if i = j then NONE else (* keep searching *)
     raise find_split_exp (* stop now *)
             "Terms are not identical upto a free varaible! (Bound)"
-  | find_term_split (a, b) =
+  | find_term_split _ =
     raise find_split_exp (* stop now *)
             "Terms are not identical upto a free varaible! (Other)";
 
@@ -160,7 +152,7 @@
            probably fine -- there is probably only one anyway. *)
         (case get_first (Seq.pull o solve_by_splitth th) splitths of
           NONE => split th
-        | SOME (solved_th, more) => solved_th);
+        | SOME (solved_th, _) => solved_th);
     in
       recsplitf genth
     end;