--- 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) =