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;