src/Pure/Isar/proof_context.ML
changeset 56007 1b61dfbcf9a4
parent 56002 2028467b4df4
child 56025 d74fed45fa8b
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 09 17:37:34 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 09 17:40:02 2014 +0100
@@ -382,7 +382,7 @@
     val tsig = tsig_of ctxt;
     val class_space = Type.class_space tsig;
 
-    val name = Type.cert_class tsig (Type.intern_class tsig xname)
+    val name = Type.cert_class tsig (Name_Space.intern class_space xname)
       handle TYPE (msg, _, _) =>
         error (msg ^ Position.here pos ^
           Markup.markup_report (Completion.reported_text