src/ZF/ind_syntax.ML
changeset 8819 d04923e183c7
parent 7694 20121c9dc1a6
child 12243 a2c0aaf94460
     1.1 --- a/src/ZF/ind_syntax.ML	Fri May 05 22:35:51 2000 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Fri May 05 22:37:04 2000 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4  
     1.5  (*read a constructor specification*)
     1.6  fun read_construct sign (id, sprems, syn) =
     1.7 -    let val prems = map (readtm sign FOLogic.oT) sprems
     1.8 +    let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
     1.9          val args = map (#1 o dest_mem) prems
    1.10          val T = (map (#2 o dest_Free) args) ---> iT
    1.11                  handle TERM _ => error