src/HOL/Tools/SMT/z3_proof_parser.ML
changeset 40627 becf5d5187cc
parent 40579 98ebd2300823
child 40662 798aad2229c0
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -256,7 +256,7 @@
     1.4  
     1.5  fun parse_line _ _ (st as ((SOME _, _), _)) = st
     1.6    | parse_line scan line ((_, line_no), cx) =
     1.7 -      let val st = ((line_no, cx), explode line)
     1.8 +      let val st = ((line_no, cx), raw_explode line)
     1.9        in
    1.10          (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of
    1.11            (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx')
    1.12 @@ -299,7 +299,7 @@
    1.13    (fn sign => nat_num >> sign)) st
    1.14  
    1.15  val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
    1.16 -  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
    1.17 +  member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
    1.18  fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
    1.19  
    1.20  fun sym st =