src/HOLCF/fixrec_package.ML

 Recursive function definition package for HOLCF.
 *)
 
 signature FIXREC_PACKAGE =
 sig
-  val add_fixrec: bool -> ((string * Attrib.src list) * string) list list
-    -> theory -> theory
-  val add_fixrec_i: bool -> ((string * theory attribute list) * term) list list
-    -> theory -> theory
-  val add_fixpat: (string * Attrib.src list) * string list
-    -> theory -> theory
-  val add_fixpat_i: (string * theory attribute list) * term list
-    -> theory -> theory
+  val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
+  val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
+  val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
+  val add_fixpat_i: (string * attribute list) * term list -> theory -> theory
 end;
 
 structure FixrecPackage: FIXREC_PACKAGE =
 struct
 

       val eqn_blocks = unconcat lengths ((names ~~ eqn_ts') ~~ atts);
       val simps = List.concat (map (make_simps thy') (unfold_thms ~~ eqn_blocks));
       val (simp_thms, thy'') = PureThy.add_thms simps thy';
       
       val simp_names = map (fn name => name^"_simps") cnames;
-      val simp_attribute = rpair [Attrib.theory Simplifier.simp_add];
+      val simp_attribute = rpair [Simplifier.simp_add];
       val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
     in
       (snd o PureThy.add_thmss simps') thy''
     end
     else thy'
   end;
 
-val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.global_attribute;
+val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute;
 val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I);
 
 
 (*************************************************************************)
 (******************************** Fixpat *********************************)

     val simps = map (fix_pat thy) ts;
   in
     (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   end;
 
-val add_fixpat = gen_add_fixpat Sign.read_term Attrib.global_attribute;
+val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute;
 val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
 
 
 (*************************************************************************)
 (******************************** Parsers ********************************)