Sign.restore_naming -- slightly more robust;
authorwenzelm
Thu Feb 18 23:37:43 2010 +0100 (2010-02-18)
changeset 35203ef65a2218c31
parent 35202 48721d3d77e7
child 35204 214ec053128e
Sign.restore_naming -- slightly more robust;
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tools/repdef.ML
     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,
     2.1 --- a/src/HOLCF/Tools/repdef.ML	Thu Feb 18 23:08:31 2010 +0100
     2.2 +++ b/src/HOLCF/Tools/repdef.ML	Thu Feb 18 23:37:43 2010 +0100
     2.3 @@ -139,7 +139,7 @@
     2.4        |> PureThy.add_thms
     2.5          [((Binding.prefix_name "REP_" name,
     2.6            Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])]
     2.7 -      ||> Sign.parent_path;
     2.8 +      ||> Sign.restore_naming thy4;
     2.9  
    2.10      val rep_info =
    2.11        { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm };