# HG changeset patch
# User wenzelm
# Date 1428516858 -7200
# Node ID 8ed8cc21c8a10d1f82db145ff6a527d3f83529c3
# Parent  ea06500bb0925d112f686338211b77a75c25a7a9
tuned;

diff -r ea06500bb092 -r 8ed8cc21c8a1 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Apr 08 19:58:52 2015 +0200
+++ b/src/Tools/induct.ML	Wed Apr 08 20:14:18 2015 +0200
@@ -165,11 +165,11 @@
 
 (* rotate k premises to the left by j, skipping over first j premises *)
 
-fun rotate_conv 0 j 0 = Conv.all_conv
+fun rotate_conv 0 _ 0 = Conv.all_conv
   | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1)
   | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k);
 
-fun rotate_tac j 0 = K all_tac
+fun rotate_tac _ 0 = K all_tac
   | rotate_tac j k = SUBGOAL (fn (goal, i) =>
       CONVERSION (rotate_conv
         j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
@@ -603,7 +603,7 @@
 fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
       let
         val x = Name.clean (Variable.revert_fixed ctxt z);
-        fun index i [] = []
+        fun index _ [] = []
           | index i (y :: ys) =
               if x = y then x ^ string_of_int i :: index (i + 1) ys
               else y :: index i ys;
@@ -826,17 +826,14 @@
       if null inst then `Rule_Cases.get r
       else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
         |> pair (Rule_Cases.get r);
-
-    fun ruleq goal =
+  in
+    fn st =>
       (case opt_rule of
         SOME r => Seq.single (inst_rule r)
       | NONE =>
           (get_coinductP ctxt goal @ get_coinductT ctxt inst)
           |> tap (trace_rules ctxt coinductN)
-          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
-  in
-    fn st =>
-      ruleq goal
+          |> Seq.of_list |> Seq.maps (Seq.try inst_rule))
       |> Seq.maps (Rule_Cases.consume ctxt [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
         guess_instance ctxt rule i st