src/Pure/sorts.ML
changeset 3783 37fb4f64eb9d
parent 3633 1884b433c6a5
child 7067 601f930d3739
     1.1 --- a/src/Pure/sorts.ML	Mon Oct 06 18:39:25 1997 +0200
     1.2 +++ b/src/Pure/sorts.ML	Mon Oct 06 18:39:54 1997 +0200
     1.3 @@ -65,11 +65,8 @@
     1.4  
     1.5  (* print sorts and arities *)
     1.6  
     1.7 -fun str_of_classrel (c1, c2) = c1 ^ " < " ^ c2;
     1.8 -
     1.9 -fun str_of_sort [c] = c
    1.10 -  | str_of_sort cs = enclose "{" "}" (commas cs);
    1.11 -
    1.12 +val str_of_sort = Syntax.simple_str_of_sort;
    1.13 +fun str_of_classrel (c1, c2) = str_of_sort [c1] ^ " < " ^ str_of_sort [c2];
    1.14  fun str_of_dom Ss = enclose "(" ")" (commas (map str_of_sort Ss));
    1.15  
    1.16  fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
    1.17 @@ -141,7 +138,7 @@
    1.18  
    1.19  fun mg_dom arities a c =
    1.20    (case assoc2 (arities, (a, c)) of
    1.21 -    None => raise_type ("No way to get " ^ a ^ "::" ^ c ^ ".") [] []
    1.22 +    None => raise TYPE ("No way to get " ^ a ^ "::" ^ c ^ ".", [], [])
    1.23    | Some Ss => Ss);
    1.24  
    1.25  fun mg_domain _ _ _ [] = sys_error "mg_domain"  (*don't know number of args!*)