src/HOL/Nominal/nominal_datatype.ML

 
     fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
       | 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 =
       let val xs = Long_Name.explode s;
       in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;