Sign.restore_naming -- slightly more robust;

--- a/src/HOLCF/Tools/pcpodef.ML	Thu Feb 18 23:08:31 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Thu Feb 18 23:37:43 2010 +0100
@@ -100,7 +100,7 @@
           ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
           ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
           ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
-      ||> Sign.parent_path;
+      ||> Sign.restore_naming thy2;
     val cpo_info : cpo_info =
       { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
         cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
@@ -139,7 +139,7 @@
           ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
           ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
           ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
-      ||> Sign.parent_path;
+      ||> Sign.restore_naming thy2;
     val pcpo_info =
       { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
         Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,

--- a/src/HOLCF/Tools/repdef.ML	Thu Feb 18 23:08:31 2010 +0100
+++ b/src/HOLCF/Tools/repdef.ML	Thu Feb 18 23:37:43 2010 +0100
@@ -139,7 +139,7 @@
       |> PureThy.add_thms
         [((Binding.prefix_name "REP_" name,
           Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])]
-      ||> Sign.parent_path;
+      ||> Sign.restore_naming thy4;
 
     val rep_info =
       { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm };