src/HOL/Nominal/nominal_inductive.ML
changeset 33368 b1cf34f1855c
parent 33049 c38f02fdf35d
child 33666 e49bfeb0d822
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Oct 30 18:33:21 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Nov 01 15:24:45 2009 +0100
     1.3 @@ -158,7 +158,7 @@
     1.4          [] => ()
     1.5        | xs => error ("Missing equivariance theorem for predicate(s): " ^
     1.6            commas_quote xs));
     1.7 -    val induct_cases = map fst (fst (RuleCases.get (the
     1.8 +    val induct_cases = map fst (fst (Rule_Cases.get (the
     1.9        (Induct.lookup_inductP ctxt (hd names)))));
    1.10      val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
    1.11      val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
    1.12 @@ -547,7 +547,7 @@
    1.13        let
    1.14          val rec_name = space_implode "_" (map Long_Name.base_name names);
    1.15          val rec_qualified = Binding.qualify false rec_name;
    1.16 -        val ind_case_names = RuleCases.case_names induct_cases;
    1.17 +        val ind_case_names = Rule_Cases.case_names induct_cases;
    1.18          val induct_cases' = Inductive.partition_rules' raw_induct
    1.19            (intrs ~~ induct_cases); 
    1.20          val thss' = map (map atomize_intr) thss;
    1.21 @@ -558,9 +558,9 @@
    1.22            (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
    1.23          val strong_induct =
    1.24            if length names > 1 then
    1.25 -            (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
    1.26 +            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
    1.27            else (strong_raw_induct RSN (2, rev_mp),
    1.28 -            [ind_case_names, RuleCases.consumes 1]);
    1.29 +            [ind_case_names, Rule_Cases.consumes 1]);
    1.30          val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
    1.31            ((rec_qualified (Binding.name "strong_induct"),
    1.32              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
    1.33 @@ -572,12 +572,12 @@
    1.34          LocalTheory.note Thm.generatedK
    1.35            ((rec_qualified (Binding.name "strong_inducts"),
    1.36              [Attrib.internal (K ind_case_names),
    1.37 -             Attrib.internal (K (RuleCases.consumes 1))]),
    1.38 +             Attrib.internal (K (Rule_Cases.consumes 1))]),
    1.39             strong_inducts) |> snd |>
    1.40          LocalTheory.notes Thm.generatedK (map (fn ((name, elim), (_, cases)) =>
    1.41              ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
    1.42 -              [Attrib.internal (K (RuleCases.case_names (map snd cases))),
    1.43 -               Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
    1.44 +              [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
    1.45 +               Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
    1.46            (strong_cases ~~ induct_cases')) |> snd
    1.47        end)
    1.48        (map (map (rulify_term thy #> rpair [])) vc_compat)