src/HOL/Tools/primrec_package.ML
changeset 18688 abf0f018b5ec
parent 18678 dd0c569fa43d
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Sat Jan 14 17:20:51 2006 +0100
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat Jan 14 22:25:34 2006 +0100
     1.3 @@ -258,7 +258,7 @@
     1.4      val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
     1.5      val thy''' = thy''
     1.6        |> (snd o PureThy.add_thmss [(("simps", simps'),
     1.7 -           [Simplifier.simp_add_global, RecfunCodegen.add NONE])])
     1.8 +           [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE])])
     1.9        |> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
    1.10        |> Theory.parent_path
    1.11    in