diff -r 98d35a7368bd -r fb579401dc26 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 26 21:10:42 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 26 21:46:04 2012 +0100
@@ -224,7 +224,7 @@
     "using " ^ space_implode " " (map string_for_label ls) ^ " "
 
 fun command_call name [] =
-    name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
+    name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
 
 fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =