# HG changeset patch
# User wenzelm
# Date 876157189 -7200
# Node ID 5802db9417182d516933516d9766c1ed0cf6ad1a
# Parent  51bd5c0954c63a923d7f9037f1a2272a83b10ea8
tuned read_cterms;

diff -r 51bd5c0954c6 -r 5802db941718 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Oct 06 18:57:17 1997 +0200
+++ b/src/Pure/thm.ML	Mon Oct 06 18:59:49 1997 +0200
@@ -274,21 +274,22 @@
 (*read a list of terms, matching them against a list of expected types.
   NO disambiguation of alternative parses via type-checking -- it is just
   not practical.*)
-fun read_cterms sign (bs, Ts) =
+fun read_cterms sg (bs, Ts) =
   let
-    val {tsig, syn, ...} = Sign.rep_sg sign;
+    val {tsig, syn, ...} = Sign.rep_sg sg;
     fun read (b, T) =
       (case Syntax.read syn T b of
         [t] => t
       | _  => error ("Error or ambiguity in parsing of " ^ b));
 
-    val prt = setmp Syntax.show_brackets true (Sign.pretty_term sign);
-    val prT = Sign.pretty_typ sign;
+    val prt = setmp Syntax.show_brackets true (Sign.pretty_term sg);
+    val prT = Sign.pretty_typ sg;
     val (us, _) =
-      Type.infer_types prt prT tsig (Sign.const_type sign)
-        (K None) (K None) [] true (map (Sign.certify_typ sign) Ts)
-        (ListPair.map read (bs, Ts));
-  in map (cterm_of sign) us end
+      (* FIXME Sign.infer_types!? *)
+      Type.infer_types prt prT tsig (Sign.const_type sg) (K None) (K None)
+        (Sign.intern_const sg) (Sign.intern_tycons sg) (Sign.intern_sort sg)
+        [] true (map (Sign.certify_typ sg) Ts) (ListPair.map read (bs, Ts));
+  in map (cterm_of sg) us end
   handle TYPE (msg, _, _) => error msg
        | TERM (msg, _) => error msg;