# HG changeset patch
# User wenzelm
# Date 1120050810 -7200
# Node ID 55ffcee3b8f3aea72cde2101e07f19ba0f6cae50
# Parent  34f99c3221bbf77257f21b84fae323e9f6782f6e
Syntax.read thy;

diff -r 34f99c3221bb -r 55ffcee3b8f3 src/Pure/theory.ML
--- 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;