# HG changeset patch
# User wenzelm
# Date 1318448373 -7200
# Node ID d7e4a7ab106115fcc97b392189a59df7b7da05bc
# Parent  563caf031b506fec21851e02b5976e68571fe82e
misc tuning and clarification;

diff -r 563caf031b50 -r d7e4a7ab1061 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Oct 12 20:57:40 2011 +0200
+++ b/src/Tools/induct.ML	Wed Oct 12 21:39:33 2011 +0200
@@ -98,7 +98,7 @@
 (** variables -- ordered left-to-right, preferring right **)
 
 fun vars_of tm =
-  rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
+  rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) tm []));
 
 local
 
@@ -484,11 +484,12 @@
 
     fun inst_rule r =
       (if null insts then r
-       else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
-         |> maps (prep_inst ctxt align_left I)
-         |> Drule.cterm_instantiate) r) |>
-      (if simp then mark_constraints (Rule_Cases.get_constraints r) ctxt else I) |>
-      pair (Rule_Cases.get r);
+       else
+         (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
+           |> maps (prep_inst ctxt align_left I)
+           |> Drule.cterm_instantiate) r)
+      |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
+      |> pair (Rule_Cases.get r);
 
     val ruleq =
       (case opt_rule of
@@ -502,8 +503,9 @@
       ruleq
       |> Seq.maps (Rule_Cases.consume [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
-        let val rule' =
-          (if simp then simplified_rule' ctxt #> unmark_constraints else I) rule
+        let
+          val rule' = rule
+            |> simp ? (simplified_rule' ctxt #> unmark_constraints);
         in
           CASES (Rule_Cases.make_common (thy,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
@@ -762,7 +764,7 @@
     fun rule_cases ctxt rule cases =
       let
         val rule' = Rule_Cases.internalize_params rule;
-        val rule'' = (if simp then simplified_rule ctxt else I) rule';
+        val rule'' = rule' |> simp ? simplified_rule ctxt;
         val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
         val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
       in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;