diff -r cbc38731d42f -r 0fbed69ff081 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/Pure/axclass.ML	Wed Mar 04 19:53:18 2015 +0100
@@ -191,7 +191,7 @@
               thy2
               |> update_classrel ((c1, c2),
                 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
-                |> Drule.instantiate' [SOME (ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
+                |> Drule.instantiate' [SOME (Thm.ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
                 |> Thm.close_derivation));
 
         val proven = is_classrel thy1;
@@ -228,7 +228,7 @@
             c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
 
     val names = Name.invent Name.context Name.aT (length Ss);
-    val std_vars = map (fn a => SOME (ctyp_of thy (TVar ((a, 0), [])))) names;
+    val std_vars = map (fn a => SOME (Thm.ctyp_of thy (TVar ((a, 0), [])))) names;
 
     val completions = super_class_completions |> map (fn c1 =>
       let
@@ -396,7 +396,7 @@
     val (th', thy') = Global_Theory.store_thm (binding, th) thy;
     val th'' = th'
       |> Thm.unconstrainT
-      |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
+      |> Drule.instantiate' [SOME (Thm.ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
   in
     thy'
     |> Sign.primitive_classrel (c1, c2)
@@ -418,7 +418,7 @@
 
     val args = Name.invent_names Name.context Name.aT Ss;
     val T = Type (t, map TFree args);
-    val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
+    val std_vars = map (fn (a, S) => SOME (Thm.ctyp_of thy' (TVar ((a, 0), [])))) args;
 
     val missing_params = Sign.complete_sort thy' [c]
       |> maps (these o Option.map #params o try (get_info thy'))