src/Pure/theory.ML
changeset 8897 fb1436ca3b2e
parent 8725 0e48ee5b52db
child 9280 78a9bca983ac
     1.1 --- a/src/Pure/theory.ML	Sun May 21 14:33:46 2000 +0200
     1.2 +++ b/src/Pure/theory.ML	Sun May 21 14:35:27 2000 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4    val add_classes_i: (bclass * class list) list -> theory -> theory
     1.5    val add_classrel: (xclass * xclass) list -> theory -> theory
     1.6    val add_classrel_i: (class * class) list -> theory -> theory
     1.7 -  val add_defsort: xsort -> theory -> theory
     1.8 +  val add_defsort: string -> theory -> theory
     1.9    val add_defsort_i: sort -> theory -> theory
    1.10    val add_types: (bstring * int * mixfix) list -> theory -> theory
    1.11    val add_nonterminals: bstring list -> theory -> theory
    1.12 @@ -48,7 +48,7 @@
    1.13      -> theory -> theory
    1.14    val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
    1.15      -> theory -> theory
    1.16 -  val add_arities: (xstring * xsort list * xsort) list -> theory -> theory
    1.17 +  val add_arities: (xstring * string list * string) list -> theory -> theory
    1.18    val add_arities_i: (string * sort list * sort) list -> theory -> theory
    1.19    val add_consts: (bstring * string * mixfix) list -> theory -> theory
    1.20    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory