src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -403,7 +403,7 @@
 
 fun read_class ctxt text =
   let
-    val (c, reports) = check_class ctxt (Symbol_Pos.source_content (Syntax.read_token text));
+    val (c, reports) = check_class ctxt (Input.source_content (Syntax.read_token text));
     val _ = Position.reports reports;
   in c end;
 
@@ -471,7 +471,7 @@
 fun read_type_name ctxt flags text =
   let
     val (T, reports) =
-      check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
+      check_type_name ctxt flags (Input.source_content (Syntax.read_token text));
     val _ = Position.reports reports;
   in T end;
 
@@ -519,7 +519,7 @@
 
 fun read_const ctxt flags text =
   let
-    val (xname, pos) = Symbol_Pos.source_content (Syntax.read_token text);
+    val (xname, pos) = Input.source_content (Syntax.read_token text);
     val (t, reports) = check_const ctxt flags (xname, [pos]);
     val _ = Position.reports reports;
   in t end;