src/Pure/type.ML
changeset 19250 932a50e2332f
parent 18964 67f572e03236
child 19305 5c16895d548b
     1.1 --- a/src/Pure/type.ML	Sat Mar 11 17:30:35 2006 +0100
     1.2 +++ b/src/Pure/type.ML	Sat Mar 11 21:23:10 2006 +0100
     1.3 @@ -480,7 +480,7 @@
     1.4    | SOME Ss' =>
     1.5        if Sorts.sorts_le C (Ss, Ss') then ars
     1.6        else if Sorts.sorts_le C (Ss', Ss)
     1.7 -      then coregular pp C t (c, Ss) (ars \ (c, Ss'))
     1.8 +      then coregular pp C t (c, Ss) (remove (op =) (c, Ss') ars)
     1.9        else err_conflict pp t NONE (c, Ss) (c, Ss'));
    1.10  
    1.11  fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
    1.12 @@ -619,8 +619,7 @@
    1.13  
    1.14  fun add_abbrev naming (a, vs, rhs) tsig = tsig |> change_types (fn types =>
    1.15    let
    1.16 -    fun err msg =
    1.17 -      error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a);
    1.18 +    fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a);
    1.19      val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
    1.20        handle TYPE (msg, _, _) => err msg;
    1.21    in