diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOLCF/pcpodef_package.ML
--- a/src/HOLCF/pcpodef_package.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOLCF/pcpodef_package.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -111,7 +111,7 @@
       let
         val admissible' = option_fold_rule set_def admissible;
         val cpo_thms = [type_def, less_def, admissible'];
-        val (theory', _) =
+        val (_, theory') =
           theory
           |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.cpo"])
             (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
@@ -123,14 +123,14 @@
               (("lub_"     ^ name, typedef_lub     OF cpo_thms), []),
               (("thelub_"  ^ name, typedef_thelub  OF cpo_thms), []),
               (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
-          |>> Theory.parent_path;
+          ||> Theory.parent_path;
       in (theory', defs) end;
 
     fun make_pcpo UUmem (theory, defs as (type_def, less_def, set_def)) =
       let
         val UUmem' = option_fold_rule set_def UUmem;
         val pcpo_thms = [type_def, less_def, UUmem'];
-        val (theory', _) =
+        val (_, theory') =
           theory
           |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.pcpo"])
             (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
@@ -141,7 +141,7 @@
               ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
               ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
               ])
-          |>> Theory.parent_path;
+          ||> Theory.parent_path;
       in (theory', defs) end;
     
     fun pcpodef_result (theory, UUmem_admissible) =