--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jan 02 22:16:16 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Jan 03 00:02:15 2013 +0100
@@ -240,6 +240,10 @@
end
| NONE => (* a free or schematic variable *)
let
+ (* This assumes that distinct names are mapped to distinct names by
+ "Variable.variant_frees". This does not hold in general but
+ should hold for ATP-generated Skolem function names, since these
+ end with a digit and "variant_frees" appends letters. *)
fun fresh_up s =
[(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
val term_ts = map (do_term [] NONE) us