changeset 40627 | becf5d5187cc |
parent 40132 | 7ee65dbffa31 |
child 40720 | b770df486e5c |
--- a/src/HOL/Tools/refute.ML Fri Nov 19 23:48:07 2010 +0100 +++ b/src/HOL/Tools/refute.ML Sat Nov 20 00:53:26 2010 +0100 @@ -2955,7 +2955,7 @@ (* string -> string *) fun strip_leading_quote s = (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs) - o explode) s + o raw_explode) s (* FIXME Symbol.explode (?) *) (* Term.typ -> string *) fun string_of_typ (Type (s, _)) = s | string_of_typ (TFree (x, _)) = strip_leading_quote x