# HG changeset patch
# User wenzelm
# Date 1154287738 -7200
# Node ID 219a996d8bde147dce85b42bae6c2bb2791e9ba8
# Parent  f09a4003e12d024b157535ad1830571e9a3e1829
add_consts: proper Sign.full_name;
sortcontext_of_typ: avoid freeze_thaw, tuned;

diff -r f09a4003e12d -r 219a996d8bde src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Sun Jul 30 21:28:57 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Sun Jul 30 21:28:58 2006 +0200
@@ -357,9 +357,9 @@
     fun add_consts v raw_cs_sup raw_cs_this thy =
       let
         fun add_global_const ((c, ty), syn) thy =
-          thy
-          |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]
-          |> `(fn thy => (c, (Sign.intern_const thy c, ty)))
+          ((c, (Sign.full_name thy c, ty)),
+            thy
+            |> Sign.add_consts_i [(c, ty |> subst_clsvar v (TFree (v, Sign.defaultS thy)), syn)]);
       in
         thy
         |> fold_map add_global_const raw_cs_this
@@ -596,10 +596,13 @@
 
 type sortcontext = (string * sort) list;
 
-fun sortcontext_of_typ thy ty =
-  (typ_tfrees o fst o Type.freeze_thaw_type) ty
-  |> map (apsnd (operational_sort_of thy))
-  |> filter (not o null o snd);
+fun sortcontext_of_typ thy ty = fold_atyps
+  (fn TFree (a, S) =>
+    (case operational_sort_of thy S of
+      [] => I
+    | S' => insert (op =) (a, S'))
+  | T => raise TYPE ("Illegal schematic type variable", [T], [])) ty []
+  |> sort_wrt fst;   (* FIXME really required?!? *)
 
 datatype classlookup = Instance of (class * string) * classlookup list list
                      | Lookup of class list * (string * (int * int))