--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri May 24 11:08:25 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri May 24 16:43:37 2013 +0200
@@ -148,7 +148,7 @@
(* The number of type arguments of a constant, zero if it's monomorphic. For
(instances of) Skolem pseudoconstants, this information is encoded in the
constant name. *)
-fun num_type_args thy s =
+fun robust_const_num_type_args thy s =
if String.isPrefix skolem_const_prefix s then
s |> Long_Name.explode |> List.last |> Int.fromString |> the
else if String.isPrefix lam_lifted_prefix s then
@@ -222,7 +222,7 @@
val term_ts = map (do_term [] NONE) term_us
val T =
(if not (null type_us) andalso
- num_type_args thy s' = length type_us then
+ robust_const_num_type_args thy s' = length type_us then
let val Ts = type_us |> map (typ_of_atp ctxt) in
if new_skolem then
SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))