# HG changeset patch
# User wenzelm
# Date 954418773 -7200
# Node ID 3759be3d1ebff05d1f10e353f69d2a2c02d7d8a1
# Parent  bf129c6505debc4f9bd82635469b85d54e4fc0d2
read_def_cterms: use Sign.read_def_terms;

diff -r bf129c6505de -r 3759be3d1ebf src/Pure/thm.ML
--- 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;