src/HOLCF/Tools/pcpodef.ML
changeset 35203 ef65a2218c31
parent 35129 ed24ba6f69aa
child 35351 7425aece4ee3
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Thu Feb 18 23:08:31 2010 +0100
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Thu Feb 18 23:37:43 2010 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4            ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
     1.5            ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
     1.6            ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
     1.7 -      ||> Sign.parent_path;
     1.8 +      ||> Sign.restore_naming thy2;
     1.9      val cpo_info : cpo_info =
    1.10        { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
    1.11          cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
    1.12 @@ -139,7 +139,7 @@
    1.13            ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
    1.14            ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
    1.15            ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
    1.16 -      ||> Sign.parent_path;
    1.17 +      ||> Sign.restore_naming thy2;
    1.18      val pcpo_info =
    1.19        { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
    1.20          Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,