explicit use of unprefix;

--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Nov 26 21:09:36 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Nov 26 21:31:46 2010 +0100
@@ -48,8 +48,8 @@
 
 fun make_tnames Ts =
   let
-    fun type_name (TFree (name, _)) = implode (tl (raw_explode name))  (* FIXME Symbol.explode (?) *)
-      | type_name (Type (name, _)) = 
+    fun type_name (TFree (name, _)) = unprefix "'" name
+      | type_name (Type (name, _)) =
           let val name' = Long_Name.base_name name
           in if Syntax.is_identifier name' then name' else "x" end;
   in indexify_names (map type_name Ts) end;

--- a/src/HOL/Tools/Function/size.ML	Fri Nov 26 21:09:36 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Fri Nov 26 21:31:46 2010 +0100
@@ -71,7 +71,7 @@
     val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
       map (fn T as TFree (s, _) =>
         let
-          val name = "f" ^ implode (tl (raw_explode s));  (* FIXME Symbol.explode (?) *)
+          val name = "f" ^ unprefix "'" s;
           val U = T --> HOLogic.natT
         in
           (((s, Free (name, U)), U), name)

--- a/src/HOL/Tools/refute.ML	Fri Nov 26 21:09:36 2010 +0100
+++ b/src/HOL/Tools/refute.ML	Fri Nov 26 21:31:46 2010 +0100
@@ -2953,9 +2953,7 @@
 fun stlc_printer ctxt model T intr assignment =
   let
     (* string -> string *)
-    fun strip_leading_quote s =
-      (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
-        o raw_explode) s  (* FIXME Symbol.explode (?) *)
+    val strip_leading_quote = perhaps (try (unprefix "'"))
     (* Term.typ -> string *)
     fun string_of_typ (Type (s, _)) = s
       | string_of_typ (TFree (x, _)) = strip_leading_quote x