# HG changeset patch
# User paulson
# Date 818415592 -3600
# Node ID a1d2735f5adeef606ab07e577b1fdb5e19e6ea5f
# Parent  73b6b003c6cae70b126c494e6cde92d63e4e7747
New function read_cterms is a combination of read_def_cterm and
read_cterm.  It reads and simultaneously type-checks a list of strings.
cterm_of no longer catches exception TYPE; instead it must be caught later on
and a message printed using Sign.exn_type_msg.  More informative messages can
be printed this way.

diff -r 73b6b003c6ca -r a1d2735f5ade src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 08 10:36:36 1995 +0100
+++ b/src/Pure/thm.ML	Fri Dec 08 10:39:52 1995 +0100
@@ -27,6 +27,7 @@
   val term_of           : cterm -> term
   val cterm_of          : Sign.sg -> term -> cterm
   val read_cterm        : Sign.sg -> string * typ -> cterm
+  val read_cterms       : Sign.sg -> string list * typ list -> cterm list
   val cterm_fun         : (term -> term) -> (cterm -> cterm)
   val dest_cimplies     : cterm -> cterm * cterm
   val read_def_cterm    :
@@ -191,9 +192,8 @@
 (*create a cterm by checking a "raw" term with respect to a signature*)
 fun cterm_of sign tm =
   let val (t, T, maxidx) = Sign.certify_term sign tm
-  in Cterm {sign = sign, t = t, T = T, maxidx = maxidx}
-  end handle TYPE (msg, _, _)
-    => raise TERM ("Term not in signature\n" ^ msg, [tm]);
+  in  Cterm {sign = sign, t = t, T = T, maxidx = maxidx}
+  end;
 
 fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t);
 
@@ -217,11 +217,31 @@
     val (_, t', tye) =
           Sign.infer_types sign types sorts used freeze (ts, T');
     val ct = cterm_of sign t'
-      handle TERM (msg, _) => error msg;
+      handle TYPE arg => error (Sign.exn_type_msg sign arg)
+	   | TERM (msg, _) => error msg;
   in (ct, tye) end;
 
 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
 
+(*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) =
+  let
+    val {tsig, syn, ...} = Sign.rep_sg sign
+    fun read (b,T) =
+	case Syntax.read syn T b of
+	    [t] => t
+	  | _   => error("Error or ambiguity in parsing of " ^ b)
+    val (us,_) = Type.infer_types(tsig, Sign.const_type sign, 
+				  K None, K None, 
+				  [], true, 
+				  map (Sign.certify_typ sign) Ts, 
+				  map read (bs~~Ts))
+  in  map (cterm_of sign) us  end
+  handle TYPE arg => error (Sign.exn_type_msg sign arg)
+       | TERM (msg, _) => error msg;
+
 
 
 (*** Meta theorems ***)
@@ -484,7 +504,8 @@
 fun cert_axm sg (name, raw_tm) =
   let
     val Cterm {t, T, ...} = cterm_of sg raw_tm
-      handle TERM (msg, _) => error msg;
+      handle TYPE arg => error (Sign.exn_type_msg sg arg)
+	   | TERM (msg, _) => error msg;
   in
     assert (T = propT) "Term not of type prop";
     (name, no_vars t)