diff -r 135f7d489492 -r 3ad3e3ca2451 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- 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