--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Thu Jan 11 10:13:42 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Thu Jan 11 12:32:07 2018 +0100
@@ -990,7 +990,7 @@
let
val _ = @{assert} (arity > 0)
val is =
- upto (1, arity)
+ 1 upto arity
|> map Int.toString
val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", @{sort type})) is
val res_ty = TFree ("res" ^ "_ty", @{sort type})
@@ -1263,7 +1263,7 @@
let
val _ = @{assert} (arity > 0)
val vars =
- upto (1, arity + 1)
+ 1 upto (arity + 1)
|> map (fn i => Free ("x" ^ Int.toString i, HOLogic.boolT))
val consequent = hd vars