adapted Sign.infer_types(_simult), Sign.certify_term/prop;
authorwenzelm
Tue Feb 07 19:56:50 2006 +0100 (2006-02-07)
changeset 1896852639ad19a96
parent 18967 ea42ab6c08d1
child 18969 49aa2c8791ba
adapted Sign.infer_types(_simult), Sign.certify_term/prop;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Tue Feb 07 19:56:49 2006 +0100
     1.2 +++ b/src/Pure/theory.ML	Tue Feb 07 19:56:50 2006 +0100
     1.3 @@ -167,20 +167,19 @@
     1.4  
     1.5  fun cert_axm thy (name, raw_tm) =
     1.6    let
     1.7 -    val pp = Sign.pp thy;
     1.8 -    val (t, T, _) = Sign.certify_term pp thy raw_tm
     1.9 +    val (t, T, _) = Sign.certify_prop thy raw_tm
    1.10        handle TYPE (msg, _, _) => error msg
    1.11          | TERM (msg, _) => error msg;
    1.12    in
    1.13      Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
    1.14 -    assert (T = propT) "Term not of type prop";
    1.15 -    (name, Sign.no_vars pp t)
    1.16 +    (name, Sign.no_vars (Sign.pp thy) t)
    1.17    end;
    1.18  
    1.19  fun read_def_axm (thy, types, sorts) used (name, str) =
    1.20    let
    1.21      val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
    1.22 -    val (t, _) = Sign.infer_types (Sign.pp thy) thy types sorts used true (ts, propT);
    1.23 +    val (t, _) =
    1.24 +      Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) types sorts used true (ts, propT);
    1.25    in cert_axm thy (name, t) end
    1.26    handle ERROR msg => err_in_axm msg name;
    1.27  
    1.28 @@ -189,7 +188,8 @@
    1.29  fun inferT_axm thy (name, pre_tm) =
    1.30    let
    1.31      val pp = Sign.pp thy;
    1.32 -    val (t, _) = Sign.infer_types pp thy (K NONE) (K NONE) [] true ([pre_tm], propT);
    1.33 +    val (t, _) =
    1.34 +      Sign.infer_types pp thy (Sign.consts_of thy) (K NONE) (K NONE) [] true ([pre_tm], propT);
    1.35    in (name, Sign.no_vars pp t) end
    1.36    handle ERROR msg => err_in_axm msg name;
    1.37