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