added rep_tsig Isabelle93
authornipkow
Mon Dec 06 17:05:10 1993 +0100 (1993-12-06)
changeset 189831a9a7ab9f3
parent 188 6be0856cdf49
child 190 4ae10fc91cba
added rep_tsig
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Mon Dec 06 13:35:38 1993 +0100
     1.2 +++ b/src/Pure/type.ML	Mon Dec 06 17:05:10 1993 +0100
     1.3 @@ -21,8 +21,13 @@
     1.4  		   -> term * (indexname*typ)list
     1.5    val inst_term_tvars: type_sig * (indexname * typ)list -> term -> term
     1.6    val logical_type: type_sig -> string -> bool
     1.7 -   val logical_types: type_sig -> string list
     1.8 +  val logical_types: type_sig -> string list
     1.9    val merge: type_sig * type_sig -> type_sig
    1.10 +  val rep_tsig: type_sig ->
    1.11 +      {classes: class list, default: sort,
    1.12 +       subclass: (class * class list) list,
    1.13 +       args: (string * int) list,
    1.14 +       coreg: (string * (class * sort list) list) list}
    1.15    val thaw_vars: typ -> typ
    1.16    val tsig0: type_sig
    1.17    val type_errors: type_sig * (typ->string) -> typ * string list -> string list
    1.18 @@ -84,6 +89,7 @@
    1.19            represents the arity (ss)c
    1.20  *)
    1.21  
    1.22 +fun rep_tsig (TySg comps) = comps;
    1.23  
    1.24  val tsig0 = TySg{classes = [],
    1.25  		 default = [],