# HG changeset patch
# User wenzelm
# Date 1394383202 -3600
# Node ID 1b61dfbcf9a4a6b26fa2511ab8b0c79c5bc0d3ed
# Parent  6a4dcaf53664252726b83c6443ce52c5f7605ce9
tuned;

diff -r 6a4dcaf53664 -r 1b61dfbcf9a4 src/Pure/Isar/proof_context.ML
--- 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