--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Oct 07 15:31:47 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Oct 07 15:31:59 2015 +0200
@@ -883,8 +883,8 @@
if s = irrelevant orelse s = unknown then Term.dummy else t | t => t) t0
fun add_fake_const s =
- Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn)
- #> #2
+ Symbol_Pos.is_identifier s
+ ? (#2 o Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn))
val globals = Term.add_const_names t []
|> filter_out (String.isSubstring Long_Name.separator)