src/Tools/induct.ML
changeset 58838 59203adfc33f
parent 58826 2ed2eaabe3df
child 58893 9e0ecb66d6a7
     1.1 --- a/src/Tools/induct.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/Tools/induct.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -512,7 +512,7 @@
     1.4          in
     1.5            CASES (Rule_Cases.make_common (thy,
     1.6                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
     1.7 -            ((Method.insert_tac more_facts THEN' rtac rule' THEN_ALL_NEW
     1.8 +            ((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW
     1.9                  (if simp then TRY o trivial_tac else K all_tac)) i) st
    1.10          end)
    1.11    end;
    1.12 @@ -683,7 +683,8 @@
    1.13    in
    1.14      (case goal_concl n [] goal of
    1.15        SOME concl =>
    1.16 -        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
    1.17 +        (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
    1.18 +          resolve_tac [asm_rl]) i
    1.19      | NONE => all_tac)
    1.20    end);
    1.21  
    1.22 @@ -804,7 +805,7 @@
    1.23                |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
    1.24                |> Seq.maps (fn rule' =>
    1.25                  CASES (rule_cases ctxt rule' cases)
    1.26 -                  (rtac rule' i THEN
    1.27 +                  (resolve_tac [rule'] i THEN
    1.28                      PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
    1.29        end)
    1.30        THEN_ALL_NEW_CASES
    1.31 @@ -862,7 +863,7 @@
    1.32          |> Seq.maps (fn rule' =>
    1.33            CASES (Rule_Cases.make_common (thy,
    1.34                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
    1.35 -            (Method.insert_tac more_facts i THEN rtac rule' i) st))
    1.36 +            (Method.insert_tac more_facts i THEN resolve_tac [rule'] i) st))
    1.37    end);
    1.38  
    1.39  end;