# HG changeset patch
# User wenzelm
# Date 1176587796 -7200
# Node ID b800228434a85bc252e62e366f36ab6e4186fa06
# Parent  bbf8835c9f874b2d456d5062976cc28a630ff1f8
simplified read_axm;

diff -r bbf8835c9f87 -r b800228434a8 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Apr 14 17:38:30 2007 +0200
+++ b/src/Pure/theory.ML	Sat Apr 14 23:56:36 2007 +0200
@@ -177,13 +177,8 @@
   end;
 
 fun read_axm thy (name, str) =
-  let
-    val ts = Syntax.read (ProofContext.init thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
-    val (t, _) =
-      Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
-        (K NONE) (K NONE) Name.context true (ts, propT);
-  in cert_axm thy (name, t) end
-  handle ERROR msg => err_in_axm msg name;
+  cert_axm thy (name, Sign.read_prop thy str)
+    handle ERROR msg => err_in_axm msg name;
 
 fun inferT_axm thy (name, pre_tm) =
   let