fix infix declarations
authorhuffman
Sun, 28 Feb 2010 15:43:09 -0800
changeset 35476 8e5eb497b042
parent 35475 979019ab92eb
child 35477 b972233773dd
fix infix declarations
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/holcf_library.ML
--- 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], []);