src/HOL/Tools/SMT/z3_model.ML
changeset 40627 becf5d5187cc
parent 40579 98ebd2300823
child 40663 e080c9e68752
     1.1 --- a/src/HOL/Tools/SMT/z3_model.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_model.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4    (fn sign => nat_num >> sign))
     1.5  
     1.6  val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
     1.7 -  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
     1.8 +  member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
     1.9  val name = spaced (Scan.many1 is_char >> implode)
    1.10  
    1.11  fun $$$ s = spaced (Scan.this_string s)
    1.12 @@ -68,7 +68,7 @@
    1.13    Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
    1.14  
    1.15  fun read_cex ls =
    1.16 -  maps (cons "\n" o explode) ls
    1.17 +  maps (cons "\n" o raw_explode) ls
    1.18    |> try (fst o Scan.finite Symbol.stopper cex)
    1.19    |> the_default []
    1.20