Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
changeset 50239 fb579401dc26
parent 50218 d50119e69453
child 50256 ed9487289e04 
--- 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) =
isabelle