tuned infer_types interface;

--- a/src/Pure/theory.ML	Thu Nov 20 12:51:31 1997 +0100
+++ b/src/Pure/theory.ML	Thu Nov 20 12:51:55 1997 +0100
@@ -215,15 +215,13 @@
 fun read_axm sg (name, str) = 
   let
     val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str;
-    val (_, t, _) =
-          Sign.infer_types sg (K None) (K None) [] true (ts, propT);
+    val (t, _) = Sign.infer_types sg (K None) (K None) [] true (ts, propT);
   in cert_axm sg (name,t) end
   handle ERROR => err_in_axm name;
 
 fun inferT_axm sg (name, pre_tm) =
   let
-    val (_, t, _) =
-      Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT);
+    val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT);
   in (name, no_vars t) end
   handle ERROR => err_in_axm name;
 

--- a/src/Pure/thm.ML	Thu Nov 20 12:51:31 1997 +0100
+++ b/src/Pure/thm.ML	Thu Nov 20 12:51:55 1997 +0100
@@ -264,8 +264,7 @@
     val T' = Sign.certify_typ sign T
       handle TYPE (msg, _, _) => error msg;
     val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
-    val (_, t', tye) =
-      Sign.infer_types sign types sorts used freeze (ts, T');
+    val (t', tye) = Sign.infer_types sign types sorts used freeze (ts, T');
     val ct = cterm_of sign t'
       handle TYPE (msg, _, _) => error msg
            | TERM (msg, _) => error msg;