src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Mon Nov 26 21:10:42 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Nov 26 21:46:04 2012 +0100
@@ -974,7 +974,7 @@
   fold_map (fn (b, raw_T, mx) => fn ctxt =>
     let
       val x = Variable.check_name b;
-      val _ = Lexicon.is_identifier (no_skolem internal x) orelse
+      val _ = Symbol_Pos.is_identifier (no_skolem internal x) orelse
         error ("Illegal variable name: " ^ Binding.print b);
 
       fun cond_tvars T =