src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 46104 eb85282db54e
parent 46097 0ed9365fa9d2
child 46112 31bc296a1257
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -836,11 +836,9 @@
     1.4  
     1.5  fun assign_operator_for_const (s, T) =
     1.6    if String.isPrefix ubfp_prefix s then
     1.7 -    if is_fun_type T then xsym "\<subseteq>" "<=" ()
     1.8 -    else xsym "\<le>" "<=" ()
     1.9 +    xsym "\<le>" "<=" ()
    1.10    else if String.isPrefix lbfp_prefix s then
    1.11 -    if is_fun_type T then xsym "\<supseteq>" ">=" ()
    1.12 -    else xsym "\<ge>" ">=" ()
    1.13 +    xsym "\<ge>" ">=" ()
    1.14    else if original_name s <> s then
    1.15      assign_operator_for_const (strip_first_name_sep s |> snd, T)
    1.16    else