src/HOL/Nominal/nominal_datatype.ML

--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -723,7 +723,7 @@
       | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
       | reindex dt = dt;
 
-    fun strip_suffix i s = implode (List.take (explode s, size s - i));
+    fun strip_suffix i s = implode (List.take (raw_explode s, size s - i));  (* FIXME Symbol.explode (?) *)
 
     (** strips the "_Rep" in type names *)
     fun strip_nth_name i s =