# HG changeset patch
# User wenzelm
# Date 1303121061 -7200
# Node ID b46b47775cbe269fb05e938a74009fa19657d4ae
# Parent  6b8e28b52ae35bb26c58f7b67bbf9735bf44bd08
simplified Sorts.class_error: plain Proof.context;
tuned;

diff -r 6b8e28b52ae3 -r b46b47775cbe src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Apr 18 11:44:39 2011 +0200
+++ b/src/Pure/Isar/class.ML	Mon Apr 18 12:04:21 2011 +0200
@@ -450,15 +450,16 @@
             (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   end;
 
-fun resort_terms pp algebra consts constraints ts =
+fun resort_terms ctxt algebra consts constraints ts =
   let
-    fun matchings (Const (c_ty as (c, _))) = (case constraints c
-         of NONE => I
-          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
-              (Consts.typargs consts c_ty) sorts)
-      | matchings _ = I
+    fun matchings (Const (c_ty as (c, _))) =
+          (case constraints c of
+            NONE => I
+          | SOME sorts =>
+              fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
+      | matchings _ = I;
     val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
-      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
+      handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
     val inst = map_type_tvar
       (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
   in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
@@ -535,7 +536,7 @@
     val improve_constraints = AList.lookup (op =)
       (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
     fun resort_check ts ctxt =
-      (case resort_terms (Context.pretty ctxt) algebra consts improve_constraints ts of
+      (case resort_terms ctxt algebra consts improve_constraints ts of
         NONE => NONE
       | SOME ts' => SOME (ts', ctxt));
     val lookup_inst_param = AxClass.lookup_inst_param consts params;
@@ -560,7 +561,8 @@
         notes = Generic_Target.notes
           (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
         abbrev = Generic_Target.abbrev
-          (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
+            Generic_Target.theory_abbrev prmode ((b, mx), t)),
         declaration = K Generic_Target.theory_declaration,
         syntax_declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
diff -r 6b8e28b52ae3 -r b46b47775cbe src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Apr 18 11:44:39 2011 +0200
+++ b/src/Pure/sorts.ML	Mon Apr 18 12:04:21 2011 +0200
@@ -48,7 +48,7 @@
   val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
     -> algebra -> (sort -> sort) * algebra
   type class_error
-  val class_error: Context.pretty -> class_error -> string
+  val class_error: Proof.context -> class_error -> string
   exception CLASS_ERROR of class_error
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   val meet_sort: algebra -> typ * sort
@@ -335,14 +335,13 @@
   No_Arity of string * class |
   No_Subsort of sort * sort;
 
-fun class_error pp (No_Classrel (c1, c2)) =
-      "No class relation " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) [c1, c2]
-  | class_error pp (No_Arity (a, c)) =
-      "No type arity " ^ Syntax.string_of_arity (Syntax.init_pretty pp) (a, [], [c])
-  | class_error pp (No_Subsort (S1, S2)) =
+fun class_error ctxt (No_Classrel (c1, c2)) =
+      "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
+  | class_error ctxt (No_Arity (a, c)) =
+      "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
+  | class_error ctxt (No_Subsort (S1, S2)) =
       "Cannot derive subsort relation " ^
-      Syntax.string_of_sort (Syntax.init_pretty pp) S1 ^ " < " ^
-      Syntax.string_of_sort (Syntax.init_pretty pp) S2;
+        Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
 
 exception CLASS_ERROR of class_error;
 
diff -r 6b8e28b52ae3 -r b46b47775cbe src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Apr 18 11:44:39 2011 +0200
+++ b/src/Pure/type.ML	Mon Apr 18 12:04:21 2011 +0200
@@ -310,7 +310,7 @@
 
 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
   | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
-      handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
+      handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
 
 
 
diff -r 6b8e28b52ae3 -r b46b47775cbe src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Apr 18 11:44:39 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Apr 18 12:04:21 2011 +0200
@@ -574,18 +574,25 @@
 fun translation_error thy permissive some_thm msg sub_msg =
   if permissive
   then raise PERMISSIVE ()
-  else let
-    val err_thm = case some_thm
-     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
-      | NONE => "";
-  in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
+  else
+    let
+      val err_thm =
+        (case some_thm of
+          SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
+        | NONE => "");
+    in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
 
 fun not_wellsorted thy permissive some_thm ty sort e =
   let
-    val err_class = Sorts.class_error (Context.pretty_global thy) e;
-    val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
-      ^ Syntax.string_of_sort_global thy sort;
-  in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
+    val ctxt = Syntax.init_pretty_global thy;
+    val err_class = Sorts.class_error ctxt e;
+    val err_typ =
+      "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
+        Syntax.string_of_sort_global thy sort;
+  in
+    translation_error thy permissive some_thm "Wellsortedness error"
+      (err_typ ^ "\n" ^ err_class)
+  end;
 
 
 (* translation *)