src/HOLCF/Tools/pcpodef.ML
changeset 35021 c839a4c670c6
parent 33680 a47277e09012
child 35129 ed24ba6f69aa
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Sun Feb 07 19:33:34 2010 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4            (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
     1.5      (* transfer thms so that they will know about the new cpo instance *)
     1.6      val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
     1.7 -    fun make thm = Drule.standard (thm OF cpo_thms');
     1.8 +    fun make thm = Drule.export_without_context (thm OF cpo_thms');
     1.9      val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
    1.10        thy2
    1.11        |> Sign.add_path (Binding.name_of name)
    1.12 @@ -127,7 +127,7 @@
    1.13        |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
    1.14          (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
    1.15      val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms;
    1.16 -    fun make thm = Drule.standard (thm OF pcpo_thms');
    1.17 +    fun make thm = Drule.export_without_context (thm OF pcpo_thms');
    1.18      val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff,
    1.19            Rep_defined, Abs_defined], thy3) =
    1.20        thy2