src/Pure/sorts.ML
changeset 42385 b46b47775cbe
parent 42383 0ae4ad40d7b5
child 42387 b1965c8992c8
     1.1 --- a/src/Pure/sorts.ML	Mon Apr 18 11:44:39 2011 +0200
     1.2 +++ b/src/Pure/sorts.ML	Mon Apr 18 12:04:21 2011 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4    val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
     1.5      -> algebra -> (sort -> sort) * algebra
     1.6    type class_error
     1.7 -  val class_error: Context.pretty -> class_error -> string
     1.8 +  val class_error: Proof.context -> class_error -> string
     1.9    exception CLASS_ERROR of class_error
    1.10    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
    1.11    val meet_sort: algebra -> typ * sort
    1.12 @@ -335,14 +335,13 @@
    1.13    No_Arity of string * class |
    1.14    No_Subsort of sort * sort;
    1.15  
    1.16 -fun class_error pp (No_Classrel (c1, c2)) =
    1.17 -      "No class relation " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) [c1, c2]
    1.18 -  | class_error pp (No_Arity (a, c)) =
    1.19 -      "No type arity " ^ Syntax.string_of_arity (Syntax.init_pretty pp) (a, [], [c])
    1.20 -  | class_error pp (No_Subsort (S1, S2)) =
    1.21 +fun class_error ctxt (No_Classrel (c1, c2)) =
    1.22 +      "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
    1.23 +  | class_error ctxt (No_Arity (a, c)) =
    1.24 +      "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
    1.25 +  | class_error ctxt (No_Subsort (S1, S2)) =
    1.26        "Cannot derive subsort relation " ^
    1.27 -      Syntax.string_of_sort (Syntax.init_pretty pp) S1 ^ " < " ^
    1.28 -      Syntax.string_of_sort (Syntax.init_pretty pp) S2;
    1.29 +        Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
    1.30  
    1.31  exception CLASS_ERROR of class_error;
    1.32