src/HOL/Tools/ATP/atp_proof_reconstruct.ML
changeset 56254 a2dd9200854d
parent 56104 fd6e132ee4fb
child 56854 ddd3af5a683d
     1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -94,7 +94,7 @@
     1.4  
     1.5  fun make_tfree ctxt w =
     1.6    let val ww = "'" ^ w in
     1.7 -    TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))
     1.8 +    TFree (ww, the_default @{sort type} (Variable.def_sort ctxt (ww, ~1)))
     1.9    end
    1.10  
    1.11  exception ATP_CLASS of string list
    1.12 @@ -126,7 +126,7 @@
    1.13               Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
    1.14               forces us to use a type parameter in all cases. *)
    1.15            Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
    1.16 -            (if null clss then HOLogic.typeS else map class_of_atp_class clss))))
    1.17 +            (if null clss then @{sort type} else map class_of_atp_class clss))))
    1.18    end
    1.19  
    1.20  fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
    1.21 @@ -175,7 +175,7 @@
    1.22    else
    1.23      (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    1.24  
    1.25 -fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
    1.26 +fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT @{sort type}
    1.27  
    1.28  (* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
    1.29  fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
    1.30 @@ -184,8 +184,8 @@
    1.31  val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
    1.32  val vampire_skolem_prefix = "sK"
    1.33  
    1.34 -(* First-order translation. No types are known for variables. "HOLogic.typeT" should allow them to
    1.35 -   be inferred. *)
    1.36 +(* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
    1.37 +   should allow them to be inferred. *)
    1.38  fun term_of_atp ctxt textual sym_tab =
    1.39    let
    1.40      val thy = Proof_Context.theory_of ctxt
    1.41 @@ -206,7 +206,7 @@
    1.42              if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
    1.43                @{const True}
    1.44              else
    1.45 -              list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
    1.46 +              list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
    1.47            end
    1.48          else
    1.49            (case unprefix_and_unascii const_prefix s of
    1.50 @@ -248,7 +248,8 @@
    1.51                         NONE)
    1.52                      |> (fn SOME T => T
    1.53                           | NONE =>
    1.54 -                           map slack_fastype_of term_ts ---> the_default HOLogic.typeT opt_T)
    1.55 +                           map slack_fastype_of term_ts --->
    1.56 +                            the_default (Type_Infer.anyT @{sort type}) opt_T)
    1.57                    val t =
    1.58                      if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
    1.59                      else Const (unproxify_const s', T)
    1.60 @@ -274,7 +275,7 @@
    1.61                    SOME T => map slack_fastype_of term_ts ---> T
    1.62                  | NONE =>
    1.63                    map slack_fastype_of ts --->
    1.64 -                  (case tys of [ty] => typ_of_atp_type ctxt ty | _ => HOLogic.typeT))
    1.65 +                  (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT @{sort type}))
    1.66                val t =
    1.67                  (case unprefix_and_unascii fixed_var_prefix s of
    1.68                    SOME s => Free (s, T)