src/Pure/axclass.ML
changeset 22385 cc2be3315e72
parent 21953 ab834c5c3858
child 22570 f166a5416b3f
     1.1 --- a/src/Pure/axclass.ML	Fri Mar 02 15:43:15 2007 +0100
     1.2 +++ b/src/Pure/axclass.ML	Fri Mar 02 15:43:16 2007 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4      ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
     1.5    val define_class_i: bstring * class list -> string list ->
     1.6      ((bstring * attribute list) * term list) list -> theory -> class * theory
     1.7 +  val read_param: theory -> string -> string
     1.8    val axiomatize_class: bstring * xstring list -> theory -> theory
     1.9    val axiomatize_class_i: bstring * class list -> theory -> theory
    1.10    val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
    1.11 @@ -269,8 +270,6 @@
    1.12  
    1.13  (** class definitions **)
    1.14  
    1.15 -local
    1.16 -
    1.17  fun read_param thy raw_t =
    1.18    let
    1.19      val t = Sign.read_term thy raw_t
    1.20 @@ -279,6 +278,8 @@
    1.21      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    1.22    end;
    1.23  
    1.24 +local
    1.25 +
    1.26  fun def_class prep_class prep_att prep_param prep_propp
    1.27      (bclass, raw_super) raw_params raw_specs thy =
    1.28    let