# HG changeset patch
# User wenzelm
# Date 1086805472 -7200
# Node ID f83f0a7053b50efb5787801f9193c2fa95f3bcc4
# Parent  e993eabc7197c6594bc893a57e0d55d06a212946
Sign.is_logtype;

diff -r e993eabc7197 -r f83f0a7053b5 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Jun 09 18:57:18 2004 +0200
+++ b/src/Pure/theory.ML	Wed Jun 09 20:24:32 2004 +0200
@@ -272,7 +272,7 @@
 (*some duplication of code with read_def_cterm*)
 fun read_def_axm (sg, types, sorts) used (name, str) =
   let
-    val ts = Syntax.read (Sign.syn_of sg) propT str;
+    val ts = Syntax.read (Sign.is_logtype sg) (Sign.syn_of sg) propT str;
     val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT);
   in cert_axm sg (name, t) end
   handle ERROR => err_in_axm name;