src/Pure/theory.ML
changeset 20155 da0505518e69
parent 19806 f860b7a98445
child 20392 88cab786d024
     1.1 --- a/src/Pure/theory.ML	Wed Jul 19 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Jul 19 12:11:57 2006 +0200
     1.3 @@ -195,7 +195,8 @@
     1.4    let
     1.5      val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     1.6      val (t, _) =
     1.7 -      Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) types sorts used true (ts, propT);
     1.8 +      Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
     1.9 +        types sorts (Name.make_context used) true (ts, propT);
    1.10    in cert_axm thy (name, t) end
    1.11    handle ERROR msg => err_in_axm msg name;
    1.12  
    1.13 @@ -205,7 +206,8 @@
    1.14    let
    1.15      val pp = Sign.pp thy;
    1.16      val (t, _) =
    1.17 -      Sign.infer_types pp thy (Sign.consts_of thy) (K NONE) (K NONE) [] true ([pre_tm], propT);
    1.18 +      Sign.infer_types pp thy (Sign.consts_of thy)
    1.19 +        (K NONE) (K NONE) Name.context true ([pre_tm], propT);
    1.20    in (name, Sign.no_vars pp t) end
    1.21    handle ERROR msg => err_in_axm msg name;
    1.22