# HG changeset patch
# User wenzelm
# Date 1146495910 -7200
# Node ID a4c7905947378be2ef5ddf9fd1f392ba18e980da
# Parent  cfdab6a91332d0ee3a7a9c5f0cf3cea331b47cab
of_sort: simplified derivation;

diff -r cfdab6a91332 -r a4c790594737 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon May 01 17:05:09 2006 +0200
+++ b/src/Pure/axclass.ML	Mon May 01 17:05:10 2006 +0200
@@ -420,42 +420,31 @@
     | NONE => error ("Cannot derive type arity " ^ Sign.string_of_arity thy (t, Ss, [c])))
   end;
 
-fun derive_type thy hyps =
-  let
-    fun derive (Type (a, Ts)) S =
-          let val Ss = Sign.arity_sorts thy a S
-          in map (apply_arity thy a (map2 (fn T => fn S => S ~~ derive T S) Ts Ss)) S end
-      | derive (TFree (a, [])) S =
-          weaken_subsort thy (the_default [] (AList.lookup (op =) hyps a)) S
-      | derive T _ = error ("Illegal occurrence of type variable " ^
-          setmp show_sorts true (Sign.string_of_typ thy) T);
-  in derive end;
+fun derive_type _ (_, []) = []
+  | derive_type thy (typ, sort) =
+      let
+        val hyps = Term.fold_atyps
+            (fn T as TFree (_, S) => insert (eq_fst op =) (T, S)
+              | T as TVar (_, S) => insert (eq_fst op =) (T, S)
+              | _ => I) typ []
+          |> map (fn (T, S) => (T, S ~~ Drule.sort_triv thy (T, S)));
+
+        fun derive (Type (a, Ts)) S =
+              let
+                val Ss = Sign.arity_sorts thy a S;
+                val ds = map (fn (T, S) => S ~~ derive T S) (Ts ~~ Ss);
+              in map (apply_arity thy a ds) S end
+          | derive T S = weaken_subsort thy (the_default [] (AList.lookup (op =) hyps T)) S;
+
+        val ths = derive typ sort;
+      in map (store_type thy) (map (pair typ) sort ~~ ths) end;
 
 in
 
 fun of_sort thy (typ, sort) =
   let
     fun lookup () = AList.lookup (op =) (Typtab.lookup_list (#types (get_instances thy)) typ);
-    val sort' = filter (is_none o lookup ()) sort;
-    val _ = conditional (not (null sort')) (fn () =>
-      let
-        val vars = Term.fold_atyps (insert (op =)) typ [];
-        val renaming =
-          map2 (fn T => fn a => (T, (a, case T of TFree (_, S) => S | TVar (_, S) => S)))
-            vars (Term.invent_names [] "'a" (length vars));
-        val typ' = typ |> Term.map_atyps
-          (fn T => TFree (#1 (the (AList.lookup (op =) renaming T)), []));
-
-        val hyps = renaming |> map (fn (_, (a, S)) => (a, S ~~ (S |> map (fn c =>
-          Thm.assume (Thm.cterm_of thy (Logic.mk_inclass (TFree (a, []), c)))))));
-        val inst = renaming |> map (fn (T, (a, S)) =>
-          pairself (Thm.ctyp_of thy) (TVar ((a, 0), S), T));
-
-        val ths =
-          derive_type thy hyps typ' sort'
-          |> map (Thm.instantiate (inst, []));
-        val _ = map (store_type thy) (map (pair typ) sort' ~~ ths);
-      in () end);
+    val _ = derive_type thy (typ, filter (is_none o lookup ()) sort);
   in map (the o lookup ()) sort end;
 
 end;