src/Tools/induct.ML
changeset 58957 c9e744ea8a38
parent 58956 a816aa3ff391
child 59057 5b649fb2f2e1
     1.1 --- a/src/Tools/induct.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/Tools/induct.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    val rulify_fallback: thm list
     1.5    val equal_def: thm
     1.6    val dest_def: term -> (term * term) option
     1.7 -  val trivial_tac: int -> tactic
     1.8 +  val trivial_tac: Proof.context -> int -> tactic
     1.9  end;
    1.10  
    1.11  signature INDUCT =
    1.12 @@ -67,7 +67,7 @@
    1.13    val rulify_tac: Proof.context -> int -> tactic
    1.14    val simplified_rule: Proof.context -> thm -> thm
    1.15    val simplify_tac: Proof.context -> int -> tactic
    1.16 -  val trivial_tac: int -> tactic
    1.17 +  val trivial_tac: Proof.context -> int -> tactic
    1.18    val rotate_tac: int -> int -> int -> tactic
    1.19    val internalize: Proof.context -> int -> thm -> thm
    1.20    val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
    1.21 @@ -513,7 +513,7 @@
    1.22            CASES (Rule_Cases.make_common (thy,
    1.23                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
    1.24              ((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW
    1.25 -                (if simp then TRY o trivial_tac else K all_tac)) i) st
    1.26 +                (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
    1.27          end)
    1.28    end;
    1.29  
    1.30 @@ -810,7 +810,7 @@
    1.31                      PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
    1.32        end)
    1.33        THEN_ALL_NEW_CASES
    1.34 -        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
    1.35 +        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
    1.36           THEN_ALL_NEW rulify_tac ctxt);
    1.37  
    1.38  val induct_tac = gen_induct_tac (K I);