src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Fri May 05 22:35:51 2000 +0200
+++ b/src/ZF/ind_syntax.ML	Fri May 05 22:37:04 2000 +0200
@@ -78,7 +78,7 @@
 
 (*read a constructor specification*)
 fun read_construct sign (id, sprems, syn) =
-    let val prems = map (readtm sign FOLogic.oT) sprems
+    let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
         val args = map (#1 o dest_mem) prems
         val T = (map (#2 o dest_Free) args) ---> iT
                 handle TERM _ => error