Syntax.read thy;
authorwenzelm
Wed Jun 29 15:13:30 2005 +0200 (2005-06-29)
changeset 1660055ffcee3b8f3
parent 16599 34f99c3221bb
child 16601 ee8eefade568
Syntax.read thy;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Wed Jun 29 15:13:29 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Jun 29 15:13:30 2005 +0200
     1.3 @@ -216,7 +216,7 @@
     1.4  
     1.5  fun read_def_axm (thy, types, sorts) used (name, str) =
     1.6    let
     1.7 -    val ts = Syntax.read (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     1.8 +    val ts = Syntax.read 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 => err_in_axm name;