# HG changeset patch
# User wenzelm
# Date 1222521636 -7200
# Node ID 73b380ba174373a48efa24de73e94ae442d52c78
# Parent  f66ca5b982b4c081ce778a4857ba5c16f3d180f3
proper transfer of theorems that involve classes being instantiated here;

diff -r f66ca5b982b4 -r 73b380ba1743 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Sat Sep 27 14:26:06 2008 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Sat Sep 27 15:20:36 2008 +0200
@@ -107,19 +107,21 @@
     fun make_cpo admissible (type_def, less_def, set_def) theory =
       let
         val admissible' = fold_rule (the_list set_def) admissible;
-        val cpo_thms = [type_def, less_def, admissible'];
+        val cpo_thms = map (Thm.transfer theory) [type_def, less_def, admissible'];
+        val theory' = theory
+          |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"])
+            (Tactic.rtac (typedef_cpo OF cpo_thms) 1);
+        val cpo_thms' = map (Thm.transfer theory') cpo_thms;
       in
-        theory
-        |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"])
-          (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
+        theory'
         |> Sign.add_path name
         |> PureThy.add_thms
             ([(("adm_" ^ name, admissible'), []),
-              (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []),
-              (("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []),
-              (("lub_"     ^ name, typedef_lub     OF cpo_thms), []),
-              (("thelub_"  ^ name, typedef_thelub  OF cpo_thms), []),
-              (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
+              (("cont_" ^ Rep_name, cont_Rep OF cpo_thms'), []),
+              (("cont_" ^ Abs_name, cont_Abs OF cpo_thms'), []),
+              (("lub_"     ^ name, typedef_lub     OF cpo_thms'), []),
+              (("thelub_"  ^ name, typedef_thelub  OF cpo_thms'), []),
+              (("compact_" ^ name, typedef_compact OF cpo_thms'), [])])
         |> snd
         |> Sign.parent_path
       end;
@@ -127,19 +129,21 @@
     fun make_pcpo UUmem (type_def, less_def, set_def) theory =
       let
         val UUmem' = fold_rule (the_list set_def) UUmem;
-        val pcpo_thms = [type_def, less_def, UUmem'];
+        val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UUmem'];
+        val theory' = theory
+          |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
+            (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1);
+        val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
       in
-        theory
-        |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
-          (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
+        theory'
         |> Sign.add_path name
         |> PureThy.add_thms
-            ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
-              ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),
-              ((Rep_name ^ "_strict_iff", Rep_strict_iff OF pcpo_thms), []),
-              ((Abs_name ^ "_strict_iff", Abs_strict_iff OF pcpo_thms), []),
-              ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
-              ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
+            ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms'), []),
+              ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms'), []),
+              ((Rep_name ^ "_strict_iff", Rep_strict_iff OF pcpo_thms'), []),
+              ((Abs_name ^ "_strict_iff", Abs_strict_iff OF pcpo_thms'), []),
+              ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms'), []),
+              ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms'), [])
               ])
         |> snd
         |> Sign.parent_path