# HG changeset patch
# User wenzelm
# Date 1349275356 -7200
# Node ID 4b9034f089ebb666686ba3798d39c03da6fe6b7c
# Parent  678aa92e921cf352321cdca596d3745e0b3859c8
use explicit Type.strip_sorts_dummy to suppress sort constraints in output;

diff -r 678aa92e921c -r 4b9034f089eb src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Oct 03 16:01:07 2012 +0200
+++ b/src/Pure/Isar/class.ML	Wed Oct 03 16:42:36 2012 +0200
@@ -173,7 +173,7 @@
       in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
     fun mk_param (c, ty) =
       Pretty.str (Proof_Context.extern_const ctxt c ^ " :: " ^
-        Syntax.string_of_typ (Config.put show_sorts false ctxt) (Type.strip_sorts ty));
+        Syntax.string_of_typ ctxt (Type.strip_sorts_dummy ty));
     fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
       (SOME o Pretty.str) ("class " ^ Proof_Context.extern_class ctxt class ^ ":"),
       (SOME o Pretty.block) [Pretty.str "supersort: ",
diff -r 678aa92e921c -r 4b9034f089eb src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Oct 03 16:01:07 2012 +0200
+++ b/src/Pure/type.ML	Wed Oct 03 16:42:36 2012 +0200
@@ -61,6 +61,7 @@
   (*special treatment of type vars*)
   val sort_of_atyp: typ -> sort
   val strip_sorts: typ -> typ
+  val strip_sorts_dummy: typ -> typ
   val no_tvars: typ -> typ
   val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
   val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
@@ -335,9 +336,13 @@
 
 (* strip_sorts *)
 
-fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts)
-  | strip_sorts (TFree (x, _)) = TFree (x, [])
-  | strip_sorts (TVar (xi, _)) = TVar (xi, []);
+val strip_sorts = map_atyps
+  (fn TFree (x, _) => TFree (x, [])
+    | TVar (xi, _) => TVar (xi, []));
+
+val strip_sorts_dummy = map_atyps
+  (fn TFree (x, _) => TFree (x, dummyS)
+    | TVar (xi, _) => TVar (xi, dummyS));
 
 
 (* no_tvars *)