src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 56252 b72e0a9d62b9
parent 56245 84fc7dfa3cd4
child 57773 2719eb9d40fe
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Mar 22 18:12:08 2014 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Mar 22 18:15:09 2014 +0100
     1.3 @@ -999,15 +999,15 @@
     1.4      val is =
     1.5        upto (1, arity)
     1.6        |> map Int.toString
     1.7 -    val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)) is
     1.8 -    val res_ty = TFree ("res" ^ "_ty", HOLogic.typeS)
     1.9 +    val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", @{sort type})) is
    1.10 +    val res_ty = TFree ("res" ^ "_ty", @{sort type})
    1.11      val f_ty = arg_tys ---> res_ty
    1.12      val f = Free ("f", f_ty)
    1.13      val xs = map (fn i =>
    1.14 -      Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
    1.15 +      Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
    1.16      (*FIXME DRY principle*)
    1.17      val ys = map (fn i =>
    1.18 -      Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
    1.19 +      Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
    1.20  
    1.21      val hyp_lhs = list_comb (f, xs)
    1.22      val hyp_rhs = list_comb (f, ys)
    1.23 @@ -1018,7 +1018,7 @@
    1.24        |> HOLogic.mk_Trueprop
    1.25      fun conc_eq i =
    1.26        let
    1.27 -        val ty = TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)
    1.28 +        val ty = TFree ("arg" ^ i ^ "_ty", @{sort type})
    1.29          val x = Free ("x" ^ i, ty)
    1.30          val y = Free ("y" ^ i, ty)
    1.31          val eq = HOLogic.eq_const ty $ x $ y