--- 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