--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sun Feb 28 15:30:44 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sun Feb 28 15:43:09 2010 -0800
@@ -37,6 +37,8 @@
struct
open HOLCF_Library;
+infixr 6 ->>;
+infix -->>;
(************************** miscellaneous functions ***************************)
--- a/src/HOLCF/Tools/holcf_library.ML Sun Feb 28 15:30:44 2010 -0800
+++ b/src/HOLCF/Tools/holcf_library.ML Sun Feb 28 15:43:09 2010 -0800
@@ -7,6 +7,9 @@
structure HOLCF_Library =
struct
+infixr 6 ->>;
+infix -->>;
+
(*** Operations from Isabelle/HOL ***)
val boolT = HOLogic.boolT;
@@ -46,8 +49,8 @@
(* ->> is taken from holcf_logic.ML *)
fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
-infixr 6 ->>; val (op ->>) = mk_cfunT;
-infix -->>; val (op -->>) = Library.foldr mk_cfunT;
+val (op ->>) = mk_cfunT;
+val (op -->>) = Library.foldr mk_cfunT;
fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);