Syntax.read thy;

--- a/src/Pure/theory.ML	Wed Jun 29 15:13:29 2005 +0200
+++ b/src/Pure/theory.ML	Wed Jun 29 15:13:30 2005 +0200
@@ -216,7 +216,7 @@
 
 fun read_def_axm (thy, types, sorts) used (name, str) =
   let
-    val ts = Syntax.read (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
+    val ts = Syntax.read thy (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     val (t, _) = Sign.infer_types (Sign.pp thy) thy types sorts used true (ts, propT);
   in cert_axm thy (name, t) end
   handle ERROR => err_in_axm name;