# HG changeset patch
# User wenzelm
# Date 1515670327 -3600
# Node ID e128ab544996c956644b900a4627cc79b0248161
# Parent  90fe8c635ba02f56865e69a9b4d1646f59714ee5
proper infix;

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