# HG changeset patch
# User huffman
# Date 1267400589 28800
# Node ID 8e5eb497b0429d34771621274b9dd1e45939cc45
# Parent  979019ab92eb9a03b18f5c8cd1fce9d2f0f1266b
fix infix declarations

diff -r 979019ab92eb -r 8e5eb497b042 src/HOLCF/Tools/Domain/domain_constructors.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 ***************************)
 
diff -r 979019ab92eb -r 8e5eb497b042 src/HOLCF/Tools/holcf_library.ML
--- 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], []);