--- a/src/Pure/axclass.ML Mon Jul 06 19:58:52 2009 +0200
+++ b/src/Pure/axclass.ML Mon Jul 06 20:36:38 2009 +0200
@@ -214,7 +214,7 @@
|> snd))
end;
-fun complete_arities thy =
+fun complete_arities thy =
let
val arities = snd (get_instances thy);
val (completions, arities') = arities
@@ -575,12 +575,13 @@
fun derive_type _ (_, []) = []
| derive_type thy (typ, sort) =
let
+ val certT = Thm.ctyp_of thy;
val vars = 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 [];
val hyps = vars
- |> map (fn (T, S) => (T, Thm.sort_triv thy (T, S) ~~ S));
+ |> map (fn (T, S) => (T, Thm.of_sort (certT T, S) ~~ S));
val ths = (typ, sort)
|> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
{class_relation =