diff -r 12d79ece3f7e -r 1b5ba4e6a953 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Nov 02 20:30:40 2009 +0100
+++ b/src/Pure/pure_thy.ML	Mon Nov 02 20:34:59 2009 +0100
@@ -227,8 +227,8 @@
 
 (*** Pure theory syntax and logical content ***)
 
-val typ = SimpleSyntax.read_typ;
-val prop = SimpleSyntax.read_prop;
+val typ = Simple_Syntax.read_typ;
+val prop = Simple_Syntax.read_prop;
 
 val typeT = Syntax.typeT;
 val spropT = Syntax.spropT;