src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 62752 d09d71223e7a
parent 61358 131fc8c10402
child 66020 a31760eee09d
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Mar 29 20:53:52 2016 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Mar 29 21:17:29 2016 +0200
     1.3 @@ -87,29 +87,31 @@
     1.4  
     1.5  type atom_pool = ((string * int) * int list) list
     1.6  
     1.7 +fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range)
     1.8 +
     1.9  fun add_wacky_syntax ctxt =
    1.10    let
    1.11      val name_of = fst o dest_Const
    1.12      val thy = Proof_Context.theory_of ctxt
    1.13      val (unrep_s, thy) = thy
    1.14        |> Sign.declare_const_global ((@{binding nitpick_unrep}, @{typ 'a}),
    1.15 -        Mixfix (unrep_mixfix (), [], 1000))
    1.16 +        mixfix (unrep_mixfix (), [], 1000))
    1.17        |>> name_of
    1.18      val (maybe_s, thy) = thy
    1.19        |> Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    1.20 -        Mixfix (maybe_mixfix (), [1000], 1000))
    1.21 +        mixfix (maybe_mixfix (), [1000], 1000))
    1.22        |>> name_of
    1.23      val (abs_s, thy) = thy
    1.24        |> Sign.declare_const_global ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
    1.25 -        Mixfix (abs_mixfix (), [40], 40))
    1.26 +        mixfix (abs_mixfix (), [40], 40))
    1.27        |>> name_of
    1.28      val (base_s, thy) = thy
    1.29        |> Sign.declare_const_global ((@{binding nitpick_base}, @{typ "'a => 'a"}),
    1.30 -        Mixfix (base_mixfix (), [1000], 1000))
    1.31 +        mixfix (base_mixfix (), [1000], 1000))
    1.32        |>> name_of
    1.33      val (step_s, thy) = thy
    1.34        |> Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}),
    1.35 -        Mixfix (step_mixfix (), [1000], 1000))
    1.36 +        mixfix (step_mixfix (), [1000], 1000))
    1.37        |>> name_of
    1.38    in
    1.39      (((unrep_s, maybe_s, abs_s), (base_s, step_s)),