# HG changeset patch
# User blanchet
# Date 1444224719 -7200
# Node ID 131fc8c1040290128cd934f4cfb0aa0d8b0ddd0c
# Parent  25ca76cfa9ce334ea49328690368a8a5fcc7d66a
avoid 'legacy binding' warning

diff -r 25ca76cfa9ce -r 131fc8c10402 src/HOL/Tools/Nitpick/nitpick_model.ML
--- 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)