diff -r acb830207103 -r b770df486e5c src/HOL/Tools/Function/size.ML
--- 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)