# HG changeset patch
# User wenzelm
# Date 861207805 -7200
# Node ID f3b5af1c5a6788c4c35e6dd0cd170c53d1824f32
# Parent  97ae96c72d8c07be76e62b9cb5e5173dde221978
renamed subclass to classrel;
tune type checking error msgs;

diff -r 97ae96c72d8c -r f3b5af1c5a67 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Apr 16 18:22:10 1997 +0200
+++ b/src/Pure/sign.ML	Wed Apr 16 18:23:25 1997 +0200
@@ -161,7 +161,7 @@
   let
     fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty);
 
-    fun pretty_subclass (cl, cls) = Pretty.block
+    fun pretty_classrel (cl, cls) = Pretty.block
       (Pretty.str (cl ^ " <") :: Pretty.brk 1 ::
         Pretty.commas (map Pretty.str cls));
 
@@ -188,13 +188,13 @@
 
 
     val Sg {tsig, const_tab, syn, stamps} = sg;
-    val {classes, subclass, default, tycons, abbrs, arities} =
+    val {classes, classrel, default, tycons, abbrs, arities} =
       Type.rep_tsig tsig;
   in
     Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
     Pretty.writeln (Pretty.strs ("classes:" :: classes));
-    Pretty.writeln (Pretty.big_list "subclass:"
-                      (map pretty_subclass subclass));
+    Pretty.writeln (Pretty.big_list "classrel:"
+                      (map pretty_classrel classrel));
     Pretty.writeln (pretty_default default);
     Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
     Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
@@ -316,17 +316,20 @@
   end;
 
 
-(*Package error messages from type checking*)
+(*package error messages from type checking*)
 fun exn_type_msg sg (msg, Ts, ts) =
-    let val show_typ = string_of_typ sg
-	val show_term = string_of_term sg
-	fun term_err [] = ""
-	  | term_err [t] = "\nInvolving this term:\n" ^ show_term t
-	  | term_err ts =
-	    "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
-    in  "\nType checking error: " ^ msg ^ "\n" ^
-	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
-    end; 
+  let
+    val show_typ = string_of_typ sg;
+    val show_term = set_ap Syntax.show_brackets true (string_of_term sg);
+
+    fun term_err [] = ""
+      | term_err [t] = "\n\nInvolving this term:\n" ^ show_term t
+      | term_err ts =
+          "\n\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
+  in
+    "\nType checking error: " ^ msg ^ "\n" ^
+      cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
+  end;
 
 
 
@@ -506,10 +509,10 @@
   end;
 
 
-(* add to subclass relation *)
+(* add to classrel *)
 
 fun ext_classrel (syn, tsig, ctab) pairs =
-  (syn, Type.ext_tsig_subclass tsig pairs, ctab);
+  (syn, Type.ext_tsig_classrel tsig pairs, ctab);
 
 
 (* add to syntax *)