src/Tools/induct.ML
changeset 59972 8ed8cc21c8a1
parent 59971 ea06500bb092
child 60097 d20ca79d50e4
     1.1 --- a/src/Tools/induct.ML	Wed Apr 08 19:58:52 2015 +0200
     1.2 +++ b/src/Tools/induct.ML	Wed Apr 08 20:14:18 2015 +0200
     1.3 @@ -165,11 +165,11 @@
     1.4  
     1.5  (* rotate k premises to the left by j, skipping over first j premises *)
     1.6  
     1.7 -fun rotate_conv 0 j 0 = Conv.all_conv
     1.8 +fun rotate_conv 0 _ 0 = Conv.all_conv
     1.9    | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1)
    1.10    | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k);
    1.11  
    1.12 -fun rotate_tac j 0 = K all_tac
    1.13 +fun rotate_tac _ 0 = K all_tac
    1.14    | rotate_tac j k = SUBGOAL (fn (goal, i) =>
    1.15        CONVERSION (rotate_conv
    1.16          j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
    1.17 @@ -603,7 +603,7 @@
    1.18  fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
    1.19        let
    1.20          val x = Name.clean (Variable.revert_fixed ctxt z);
    1.21 -        fun index i [] = []
    1.22 +        fun index _ [] = []
    1.23            | index i (y :: ys) =
    1.24                if x = y then x ^ string_of_int i :: index (i + 1) ys
    1.25                else y :: index i ys;
    1.26 @@ -826,17 +826,14 @@
    1.27        if null inst then `Rule_Cases.get r
    1.28        else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
    1.29          |> pair (Rule_Cases.get r);
    1.30 -
    1.31 -    fun ruleq goal =
    1.32 +  in
    1.33 +    fn st =>
    1.34        (case opt_rule of
    1.35          SOME r => Seq.single (inst_rule r)
    1.36        | NONE =>
    1.37            (get_coinductP ctxt goal @ get_coinductT ctxt inst)
    1.38            |> tap (trace_rules ctxt coinductN)
    1.39 -          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
    1.40 -  in
    1.41 -    fn st =>
    1.42 -      ruleq goal
    1.43 +          |> Seq.of_list |> Seq.maps (Seq.try inst_rule))
    1.44        |> Seq.maps (Rule_Cases.consume ctxt [] facts)
    1.45        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
    1.46          guess_instance ctxt rule i st