src/Pure/axclass.ML

       |> Symtab.insert_list (eq_fst op =) arity'
       |> insert_arity_completions thy arity'
       |> snd))
   end;
 
-fun complete_arities thy = 
+fun complete_arities thy =
   let
     val arities = snd (get_instances thy);
     val (completions, arities') = arities
       |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities)
       |>> flat;

 fun insert_type T der (Types cache) = Types (Typtab.insert_list (eq_fst op =) (T, der) cache);
 
 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 =
               fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
             type_constructor =