Adapted to new interface of RecfunCodegen.add.
authorberghofe
Fri Jul 01 14:14:40 2005 +0200 (2005-07-01)
changeset 16646666774b0d1b0
parent 16645 a152d6b21c31
child 16647 c6d81ddebb0e
Adapted to new interface of RecfunCodegen.add.
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jul 01 14:13:40 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jul 01 14:14:40 2005 +0200
     1.3 @@ -286,7 +286,7 @@
     1.4    (#1 o PureThy.add_thmss [(("simps", simps), []),
     1.5      (("", List.concat case_thms @ size_thms @ 
     1.6            List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
     1.7 -    (("", size_thms @ rec_thms), [RecfunCodegen.add]),
     1.8 +    (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
     1.9      (("", List.concat inject),               [iff_add_global]),
    1.10      (("", List.concat distinct RL [notE]),   [Classical.safe_elim_global]),
    1.11      (("", weak_case_congs),           [cong_att])]);
     2.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Jul 01 14:13:40 2005 +0200
     2.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Jul 01 14:14:40 2005 +0200
     2.3 @@ -259,7 +259,8 @@
     2.4          (fn _ => [rtac refl 1])) eqns;
     2.5      val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
     2.6      val thy''' = thy''
     2.7 -      |> (#1 o PureThy.add_thmss [(("simps", simps'), [Simplifier.simp_add_global, RecfunCodegen.add])])
     2.8 +      |> (#1 o PureThy.add_thmss [(("simps", simps'),
     2.9 +           [Simplifier.simp_add_global, RecfunCodegen.add NONE])])
    2.10        |> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
    2.11        |> Theory.parent_path
    2.12    in
     3.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jul 01 14:13:40 2005 +0200
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Jul 01 14:14:40 2005 +0200
     3.3 @@ -248,7 +248,7 @@
     3.4                 congs wfs name R eqs;
     3.5      val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
     3.6      val simp_att = if null tcs then
     3.7 -      [Simplifier.simp_add_global, RecfunCodegen.add] else [];
     3.8 +      [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
     3.9  
    3.10      val (thy, (simps' :: rules', [induct'])) =
    3.11        thy