src/Pure/Isar/code_unit.ML

--- a/src/Pure/Isar/code_unit.ML	Tue Sep 25 13:28:35 2007 +0200
+++ b/src/Pure/Isar/code_unit.ML	Tue Sep 25 13:28:37 2007 +0200
@@ -60,7 +60,7 @@
 
 fun read_bare_const thy raw_t =
   let
-    val t = Sign.read_term thy raw_t;
+    val t = Syntax.read_term_global thy raw_t;
   in case try dest_Const t
    of SOME c_ty => c_ty
     | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)