
diff -r 90fe8c635ba0 -r e128ab544996 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- 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




