src/HOL/Tools/primrec_package.ML
changeset 18728 6790126ab5f6
parent 18688 abf0f018b5ec
child 18928 042608ffa2ec
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4    val quiet_mode: bool ref
     1.5    val add_primrec: string -> ((bstring * string) * Attrib.src list) list
     1.6      -> theory -> theory * thm list
     1.7 -  val add_primrec_i: string -> ((bstring * term) * theory attribute list) list
     1.8 +  val add_primrec_i: string -> ((bstring * term) * attribute list) list
     1.9      -> theory -> theory * thm list
    1.10  end;
    1.11  
    1.12 @@ -258,7 +258,7 @@
    1.13      val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
    1.14      val thy''' = thy''
    1.15        |> (snd o PureThy.add_thmss [(("simps", simps'),
    1.16 -           [Attrib.theory Simplifier.simp_add, RecfunCodegen.add NONE])])
    1.17 +          [Simplifier.simp_add, RecfunCodegen.add NONE])])
    1.18        |> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
    1.19        |> Theory.parent_path
    1.20    in
    1.21 @@ -270,7 +270,7 @@
    1.22    let
    1.23      val sign = Theory.sign_of thy;
    1.24      val ((names, strings), srcss) = apfst split_list (split_list eqns);
    1.25 -    val atts = map (map (Attrib.global_attribute thy)) srcss;
    1.26 +    val atts = map (map (Attrib.attribute thy)) srcss;
    1.27      val eqn_ts = map (fn s => term_of (Thm.read_cterm sign (s, propT))
    1.28        handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
    1.29      val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq)))