src/HOL/Tools/Nitpick/nitpick_isar.ML

            "Run Nitpick automatically.")
 
 type raw_param = string * string list
 
 val default_default_params =
-  [("card", "1\<midarrow>10"),
+  [("card", "1\<emdash>10"),
    ("iter", "0,1,2,4,8,12,16,20,24,28"),
    ("bits", "1,2,3,4,6,8,10,12,14,16"),
    ("bisim_depth", "9"),
    ("box", "smart"),
    ("finitize", "smart"),

 
 val set_default_raw_param =
   Data.map o fold (AList.update (op =)) o normalize_raw_param
 val default_raw_params = Data.get
 
-fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
+fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<emdash>")
 
 fun stringify_raw_param_value [] = ""
   | stringify_raw_param_value [s] = s
   | stringify_raw_param_value (s1 :: s2 :: ss) =
     s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^

       | value => SOME (do_int name value)
     fun int_range_from_string name min_int s =
       let
         val (k1, k2) =
           (case space_explode "-" s of
-             [s] => the_default (s, s) (first_field "\<midarrow>" s)
+             [s] => the_default (s, s) (first_field "\<emdash>" s)
            | ["", s2] => ("-" ^ s2, "-" ^ s2)
            | [s1, s2] => (s1, s2)
            | _ => raise Option)
           |> pairself (maxed_int_from_string min_int)
       in if k1 <= k2 then k1 upto k2 else k1 downto k2 end