read_def_cterm: minor changes;
merge_thm_sgs: improved error msg;

--- a/src/Pure/thm.ML	Tue Aug 23 19:31:05 1994 +0200
+++ b/src/Pure/thm.ML	Tue Aug 23 19:33:33 1994 +0200
@@ -185,14 +185,17 @@
 
 
 
-(** read cterms **)   (*exception ERROR*)     (* FIXME check *)
+(** read cterms **)   (*exception ERROR*)
 
 (*read term, infer types, certify term*)
 fun read_def_cterm (sign, types, sorts) (a, T) =
   let
-    val t = Syntax.read (#syn (Sign.rep_sg sign)) T a;
-    val (t', tye) = Sign.infer_types sign types sorts (t, T);
-    val ct = cterm_of sign t' handle TERM (msg, _) => error msg;
+    val T' = Sign.certify_typ sign T
+      handle TYPE (msg, _, _) => error msg;
+    val t = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
+    val (t', tye) = Sign.infer_types sign types sorts (t, T');
+    val ct = cterm_of sign t'
+      handle TERM (msg, _) => error msg;
   in (ct, tye) end;
 
 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None);
@@ -216,7 +219,7 @@
 (*merge signatures of two theorems; raise exception if incompatible*)
 fun merge_thm_sgs (th1, th2) =
   Sign.merge (pairself sign_of_thm (th1, th2))
-    handle TERM _ => raise THM ("incompatible signatures", 0, [th1, th2]);
+    handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
 
 
 (*maps object-rule to tpairs*)