avoid 'legacy binding' warning
authorblanchet
Wed Oct 07 15:31:59 2015 +0200 (2015-10-07)
changeset 61358131fc8c10402
parent 61357 25ca76cfa9ce
child 61359 e985b52c3eb3
avoid 'legacy binding' warning
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 07 15:31:47 2015 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 07 15:31:59 2015 +0200
     1.3 @@ -883,8 +883,8 @@
     1.4        if s = irrelevant orelse s = unknown then Term.dummy else t | t => t) t0
     1.5  
     1.6      fun add_fake_const s =
     1.7 -      Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn)
     1.8 -      #> #2
     1.9 +      Symbol_Pos.is_identifier s
    1.10 +      ? (#2 o Sign.declare_const_global ((Binding.name s, @{typ 'a}), NoSyn))
    1.11  
    1.12      val globals = Term.add_const_names t []
    1.13        |> filter_out (String.isSubstring Long_Name.separator)