src/HOL/Tools/Nitpick/kodkod.ML
changeset 53093 503a26723c4f
parent 50488 1b3eb579e08b
child 54816 10d48c2a3e32
equal deleted inserted replaced
53092:7e89edba3db6 53093:503a26723c4f
   879       strip_blanks (s1 :: s2 :: ss)
   879       strip_blanks (s1 :: s2 :: ss)
   880   | strip_blanks (s :: ss) = s :: strip_blanks ss
   880   | strip_blanks (s :: ss) = s :: strip_blanks ss
   881 
   881 
   882 val scan_nat =
   882 val scan_nat =
   883   Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
   883   Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
   884   >> (the o Int.fromString o space_implode "")
   884   >> (the o Int.fromString o implode)
   885 val scan_rel_name =
   885 val scan_rel_name =
   886   ($$ "s" |-- scan_nat >> pair 1
   886   ($$ "s" |-- scan_nat >> pair 1
   887    || $$ "r" |-- scan_nat >> pair 2
   887    || $$ "r" |-- scan_nat >> pair 2
   888    || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'")
   888    || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'")
   889   >> (fn ((n, j), SOME _) => (n, ~j - 1)
   889   >> (fn ((n, j), SOME _) => (n, ~j - 1)