1.1 --- a/src/Tools/induct.ML	Wed Oct 12 20:57:40 2011 +0200
     1.2 +++ b/src/Tools/induct.ML	Wed Oct 12 21:39:33 2011 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4  (** variables -- ordered left-to-right, preferring right **)
     1.5  
     1.6  fun vars_of tm =
     1.7 -  rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
     1.8 +  rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) tm []));
     1.9  
    1.10  local
    1.11  
    1.12 @@ -484,11 +484,12 @@
    1.13  
    1.14      fun inst_rule r =
    1.15        (if null insts then r
    1.16 -       else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
    1.17 -         |> maps (prep_inst ctxt align_left I)
    1.18 -         |> Drule.cterm_instantiate) r) |>
    1.19 -      (if simp then mark_constraints (Rule_Cases.get_constraints r) ctxt else I) |>
    1.20 -      pair (Rule_Cases.get r);
    1.21 +       else
    1.22 +         (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
    1.23 +           |> maps (prep_inst ctxt align_left I)
    1.24 +           |> Drule.cterm_instantiate) r)
    1.25 +      |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
    1.26 +      |> pair (Rule_Cases.get r);
    1.27  
    1.28      val ruleq =
    1.29        (case opt_rule of
    1.30 @@ -502,8 +503,9 @@
    1.31        ruleq
    1.32        |> Seq.maps (Rule_Cases.consume [] facts)
    1.33        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
    1.34 -        let val rule' =
    1.35 -          (if simp then simplified_rule' ctxt #> unmark_constraints else I) rule
    1.36 +        let
    1.37 +          val rule' = rule
    1.38 +            |> simp ? (simplified_rule' ctxt #> unmark_constraints);
    1.39          in
    1.40            CASES (Rule_Cases.make_common (thy,
    1.41                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
    1.42 @@ -762,7 +764,7 @@
    1.43      fun rule_cases ctxt rule cases =
    1.44        let
    1.45          val rule' = Rule_Cases.internalize_params rule;
    1.46 -        val rule'' = (if simp then simplified_rule ctxt else I) rule';
    1.47 +        val rule'' = rule' |> simp ? simplified_rule ctxt;
    1.48          val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
    1.49          val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
    1.50        in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;