src/Pure/thm.ML
changeset 4251 f6bd8332eb32
parent 4182 47067b5db7ef
child 4254 8ae7ace96c39
     1.1 --- a/src/Pure/thm.ML	Thu Nov 20 12:51:31 1997 +0100
     1.2 +++ b/src/Pure/thm.ML	Thu Nov 20 12:51:55 1997 +0100
     1.3 @@ -264,8 +264,7 @@
     1.4      val T' = Sign.certify_typ sign T
     1.5        handle TYPE (msg, _, _) => error msg;
     1.6      val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
     1.7 -    val (_, t', tye) =
     1.8 -      Sign.infer_types sign types sorts used freeze (ts, T');
     1.9 +    val (t', tye) = Sign.infer_types sign types sorts used freeze (ts, T');
    1.10      val ct = cterm_of sign t'
    1.11        handle TYPE (msg, _, _) => error msg
    1.12             | TERM (msg, _) => error msg;