src/HOLCF/fixrec_package.ML
changeset 18728 6790126ab5f6
parent 18688 abf0f018b5ec
child 18974 593af1a1068b
     1.1 --- a/src/HOLCF/fixrec_package.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOLCF/fixrec_package.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -7,14 +7,10 @@
     1.4  
     1.5  signature FIXREC_PACKAGE =
     1.6  sig
     1.7 -  val add_fixrec: bool -> ((string * Attrib.src list) * string) list list
     1.8 -    -> theory -> theory
     1.9 -  val add_fixrec_i: bool -> ((string * theory attribute list) * term) list list
    1.10 -    -> theory -> theory
    1.11 -  val add_fixpat: (string * Attrib.src list) * string list
    1.12 -    -> theory -> theory
    1.13 -  val add_fixpat_i: (string * theory attribute list) * term list
    1.14 -    -> theory -> theory
    1.15 +  val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
    1.16 +  val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
    1.17 +  val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
    1.18 +  val add_fixpat_i: (string * attribute list) * term list -> theory -> theory
    1.19  end;
    1.20  
    1.21  structure FixrecPackage: FIXREC_PACKAGE =
    1.22 @@ -250,7 +246,7 @@
    1.23        val (simp_thms, thy'') = PureThy.add_thms simps thy';
    1.24        
    1.25        val simp_names = map (fn name => name^"_simps") cnames;
    1.26 -      val simp_attribute = rpair [Attrib.theory Simplifier.simp_add];
    1.27 +      val simp_attribute = rpair [Simplifier.simp_add];
    1.28        val simps' = map simp_attribute (simp_names ~~ unconcat lengths simp_thms);
    1.29      in
    1.30        (snd o PureThy.add_thmss simps') thy''
    1.31 @@ -258,7 +254,7 @@
    1.32      else thy'
    1.33    end;
    1.34  
    1.35 -val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.global_attribute;
    1.36 +val add_fixrec = gen_add_fixrec Sign.read_prop Attrib.attribute;
    1.37  val add_fixrec_i = gen_add_fixrec Sign.cert_prop (K I);
    1.38  
    1.39  
    1.40 @@ -286,7 +282,7 @@
    1.41      (snd o PureThy.add_thmss [((name, simps), atts)]) thy
    1.42    end;
    1.43  
    1.44 -val add_fixpat = gen_add_fixpat Sign.read_term Attrib.global_attribute;
    1.45 +val add_fixpat = gen_add_fixpat Sign.read_term Attrib.attribute;
    1.46  val add_fixpat_i = gen_add_fixpat Sign.cert_term (K I);
    1.47  
    1.48