adapted to new PureThy.add_thms etc.;
authorwenzelm
Mon Mar 13 13:18:59 2000 +0100 (2000-03-13)
changeset 8430dbd897e0d804
parent 8429 515fa7533354
child 8431 e5f8ee756a8a
adapted to new PureThy.add_thms etc.;
number cases;
src/HOL/Tools/recdef_package.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Mon Mar 13 13:17:52 2000 +0100
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Mon Mar 13 13:18:59 2000 +0100
     1.3 @@ -86,15 +86,13 @@
     1.4      val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
     1.5      val (thy, congs) = thy |> app_thms raw_congs;
     1.6      val (thy, {rules, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
     1.7 -    val thy =
     1.8 +    val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
     1.9 +    val (thy, ([rules], [induct])) =
    1.10        thy
    1.11        |> Theory.add_path bname
    1.12        |> PureThy.add_thmss [(("rules", rules), [])]
    1.13 -      |> PureThy.add_thms [(("induct", induct), [])];
    1.14 -    val result =
    1.15 -     {rules = PureThy.get_thms thy "rules",
    1.16 -      induct = PureThy.get_thm thy "induct",
    1.17 -      tcs = tcs};
    1.18 +      |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
    1.19 +    val result = {rules = rules, induct = induct, tcs = tcs};
    1.20      val thy =
    1.21        thy
    1.22        |> put_recdef name result
    1.23 @@ -120,12 +118,12 @@
    1.24  
    1.25      val (thy1, congs) = thy |> app_thms raw_congs;
    1.26      val (thy2, induct_rules) = tfl_fn thy1 name congs eqs;
    1.27 -    val thy3 =
    1.28 +    val (thy3, [induct_rules']) =
    1.29        thy2
    1.30        |> Theory.add_path bname
    1.31        |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
    1.32 -      |> Theory.parent_path;
    1.33 -  in (thy3, {induct_rules = induct_rules}) end;
    1.34 +      |>> Theory.parent_path;
    1.35 +  in (thy3, {induct_rules = induct_rules'}) end;
    1.36  
    1.37  val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
    1.38  val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;