src/HOL/Tools/inductive_package.ML
changeset 24830 a7b3ab44d993
parent 24815 f7093e90f36c
child 24861 cc669ca5f382
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Oct 04 14:42:11 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 04 14:42:47 2007 +0200
     1.3 @@ -433,7 +433,7 @@
     1.4        error (Pretty.string_of (Pretty.block
     1.5          [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop]));
     1.6  
     1.7 -    val elims = InductAttrib.find_casesS ctxt prop;
     1.8 +    val elims = Induct.find_casesS ctxt prop;
     1.9  
    1.10      val cprop = Thm.cterm_of thy prop;
    1.11      val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
    1.12 @@ -679,7 +679,7 @@
    1.13        if coind then
    1.14          (raw_induct, [RuleCases.case_names [rec_name],
    1.15            RuleCases.case_conclusion (rec_name, intr_names),
    1.16 -          RuleCases.consumes 1, InductAttrib.coinduct_set (hd cnames)])
    1.17 +          RuleCases.consumes 1, Induct.coinduct_set (hd cnames)])
    1.18        else if no_ind orelse length cnames > 1 then
    1.19          (raw_induct, [ind_case_names, RuleCases.consumes 0])
    1.20        else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
    1.21 @@ -698,7 +698,7 @@
    1.22          LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases",
    1.23            [Attrib.internal (K (RuleCases.case_names cases)),
    1.24             Attrib.internal (K (RuleCases.consumes 1)),
    1.25 -           Attrib.internal (K (InductAttrib.cases_set name)),
    1.26 +           Attrib.internal (K (Induct.cases_set name)),
    1.27             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
    1.28          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
    1.29        LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"),
    1.30 @@ -712,7 +712,7 @@
    1.31            inducts |> map (fn (name, th) => ([th],
    1.32              [Attrib.internal (K ind_case_names),
    1.33               Attrib.internal (K (RuleCases.consumes 1)),
    1.34 -             Attrib.internal (K (InductAttrib.induct_set name))])))] |> snd
    1.35 +             Attrib.internal (K (Induct.induct_set name))])))] |> snd
    1.36        end
    1.37    in (intrs', elims', induct', ctxt3) end;
    1.38