--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 17:15:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 17:32:10 2010 +0200
@@ -323,8 +323,10 @@
case strip_prefix_and_undo_ascii schematic_var_prefix a of
SOME b => Var ((b, 0), T)
| NONE =>
- if is_variable a then Var ((fix_atp_variable_name a, 0), T)
- else raise Fail ("Unexpected constant: " ^ quote a)
+ if is_tptp_variable a then
+ Var ((fix_atp_variable_name a, 0), T)
+ else
+ raise Fail ("Unexpected constant: " ^ quote a)
in list_comb (t, ts) end
in aux (SOME HOLogic.boolT) [] end