read_def_cterms: use Sign.read_def_terms;

--- a/src/Pure/thm.ML	Thu Mar 30 14:19:13 2000 +0200
+++ b/src/Pure/thm.ML	Thu Mar 30 14:19:33 2000 +0200
@@ -289,13 +289,7 @@
 (*read terms, infer types, certify terms*)
 fun read_def_cterms (sign, types, sorts) used freeze sTs =
   let
-    val syn = #syn (Sign.rep_sg sign)
-    fun read(s,T) =
-      let val T' = Sign.certify_typ sign T
-                   handle TYPE (msg, _, _) => error msg
-      in (Syntax.read syn T' s, T') end
-    val tsTs = map read sTs
-    val (ts',tye) = Sign.infer_types_simult sign types sorts used freeze tsTs;
+    val (ts', tye) = Sign.read_def_terms (sign, types, sorts) used freeze sTs;
     val cts = map (cterm_of sign) ts'
       handle TYPE (msg, _, _) => error msg
            | TERM (msg, _) => error msg;