src/HOL/Tools/refute.ML
changeset 40720 b770df486e5c
parent 40627 becf5d5187cc
child 41471 54a58904a598
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Nov 26 21:09:36 2010 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Nov 26 21:31:46 2010 +0100
     1.3 @@ -2953,9 +2953,7 @@
     1.4  fun stlc_printer ctxt model T intr assignment =
     1.5    let
     1.6      (* string -> string *)
     1.7 -    fun strip_leading_quote s =
     1.8 -      (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
     1.9 -        o raw_explode) s  (* FIXME Symbol.explode (?) *)
    1.10 +    val strip_leading_quote = perhaps (try (unprefix "'"))
    1.11      (* Term.typ -> string *)
    1.12      fun string_of_typ (Type (s, _)) = s
    1.13        | string_of_typ (TFree (x, _)) = strip_leading_quote x