src/Pure/theory.ML
changeset 22689 b800228434a8
parent 22684 a614c5f506ea
child 22697 92f8e9a8df78
     1.1 --- a/src/Pure/theory.ML	Sat Apr 14 17:38:30 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Sat Apr 14 23:56:36 2007 +0200
     1.3 @@ -177,13 +177,8 @@
     1.4    end;
     1.5  
     1.6  fun read_axm thy (name, str) =
     1.7 -  let
     1.8 -    val ts = Syntax.read (ProofContext.init thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     1.9 -    val (t, _) =
    1.10 -      Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
    1.11 -        (K NONE) (K NONE) Name.context true (ts, propT);
    1.12 -  in cert_axm thy (name, t) end
    1.13 -  handle ERROR msg => err_in_axm msg name;
    1.14 +  cert_axm thy (name, Sign.read_prop thy str)
    1.15 +    handle ERROR msg => err_in_axm msg name;
    1.16  
    1.17  fun inferT_axm thy (name, pre_tm) =
    1.18    let