# HG changeset patch
# User wenzelm
# Date 1435240593 -7200
# Node ID 58b24fea3b00977a1737536e2df3352e3f6bf4f8
# Parent  380d5a433719f277f6bb0c0401cace43728d6c59
tuned;

diff -r 380d5a433719 -r 58b24fea3b00 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Jun 25 12:13:29 2015 +0200
+++ b/src/Tools/induct.ML	Thu Jun 25 15:56:33 2015 +0200
@@ -127,15 +127,15 @@
     fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
       | conv1 k ctxt =
           Conv.rewr_conv @{thm swap_params} then_conv
-          Conv.forall_conv (conv1 (k - 1) o snd) ctxt
+          Conv.forall_conv (conv1 (k - 1) o snd) ctxt;
     fun conv2 0 ctxt = conv1 j ctxt
-      | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt
+      | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt;
   in conv2 i ctxt end;
 
 fun swap_prems_conv 0 = Conv.all_conv
   | swap_prems_conv i =
       Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
-      Conv.rewr_conv Drule.swap_prems_eq
+      Conv.rewr_conv Drule.swap_prems_eq;
 
 fun find_eq ctxt t =
   let
@@ -622,7 +622,9 @@
             val xs = rename_params (Logic.strip_params A);
             val xs' =
               (case filter (fn x' => x' = x) xs of
-                [] => xs | [_] => xs | _ => index 1 xs);
+                [] => xs
+              | [_] => xs
+              | _ => index 1 xs);
           in Logic.list_rename_params xs' A end;
         fun rename_prop prop =
           let val (As, C) = Logic.strip_horn prop
@@ -778,7 +780,7 @@
                 val adefs = nth_list atomized_defs (j - 1);
                 val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
                 val xs = nth_list arbitrary (j - 1);
-                val k = nth concls (j - 1) + more_consumes
+                val k = nth concls (j - 1) + more_consumes;
               in
                 Method.insert_tac (more_facts @ adefs) THEN'
                   (if simp then