src/Pure/sign.ML
changeset 583 550292083e66
parent 573 2fa5ef27bd0a
child 620 f787eb061618
     1.1 --- a/src/Pure/sign.ML	Tue Sep 06 13:09:58 1994 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Sep 06 13:10:38 1994 +0200
     1.3 @@ -26,8 +26,8 @@
     1.4      val is_draft: sg -> bool
     1.5      val const_type: sg -> string -> typ option
     1.6      val classes: sg -> class list
     1.7 -    val subsort: sg -> sort * sort -> bool      (* FIXME move? *)
     1.8 -    val norm_sort: sg -> sort -> sort           (* FIXME move? *)
     1.9 +    val subsort: sg -> sort * sort -> bool
    1.10 +    val norm_sort: sg -> sort -> sort
    1.11      val print_sg: sg -> unit
    1.12      val pretty_sg: sg -> Pretty.T
    1.13      val pprint_sg: sg -> pprint_args -> unit
    1.14 @@ -243,7 +243,7 @@
    1.15  
    1.16  
    1.17  
    1.18 -(** infer_types **)         (*exception ERROR*)   (* FIXME check *)
    1.19 +(** infer_types **)         (*exception ERROR*)
    1.20  
    1.21  fun infer_types sg types sorts (t, T) =
    1.22    let
    1.23 @@ -280,9 +280,6 @@
    1.24  fun ext_tsig_classes tsig classes =
    1.25    extend_tsig tsig (classes, [], [], []);
    1.26  
    1.27 -fun ext_tsig_types tsig types =
    1.28 -  extend_tsig tsig ([], [], map (fn (t, n) => ([t], n)) types, []);
    1.29 -
    1.30  (* FIXME varify_typ, rem_sorts; norm_typ (?) *)
    1.31  fun ext_tsig_abbrs tsig abbrs = Type.ext_tsig_abbrs tsig
    1.32    (map (fn (t, vs, rhs) => (t, (map (rpair 0) vs, varifyT rhs))) abbrs);