src/Pure/theory.ML
changeset 18857 c4b4fbd74ffb
parent 18763 e2b4ba340ff1
child 18943 947d3a694654
     1.1 --- a/src/Pure/theory.ML	Mon Jan 30 15:31:31 2006 +0100
     1.2 +++ b/src/Pure/theory.ML	Tue Jan 31 00:39:40 2006 +0100
     1.3 @@ -187,7 +187,7 @@
     1.4  
     1.5  fun read_def_axm (thy, types, sorts) used (name, str) =
     1.6    let
     1.7 -    val ts = Syntax.read thy (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     1.8 +    val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     1.9      val (t, _) = Sign.infer_types (Sign.pp thy) thy types sorts used true (ts, propT);
    1.10    in cert_axm thy (name, t) end
    1.11    handle ERROR msg => err_in_axm msg name;