--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Sep 13 16:44:17 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Sep 13 16:44:18 2010 +0200
@@ -15,6 +15,7 @@
(* mode *)
datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
val eq_mode : mode * mode -> bool
+ val mode_ord: mode * mode -> order
val list_fun_mode : mode list -> mode
val strip_fun_mode : mode -> mode list
val dest_fun_mode : mode -> mode list
@@ -187,6 +188,14 @@
| eq_mode (Bool, Bool) = true
| eq_mode _ = false
+fun mode_ord (Input, Output) = LESS
+ | mode_ord (Output, Input) = GREATER
+ | mode_ord (Input, Input) = EQUAL
+ | mode_ord (Output, Output) = EQUAL
+ | mode_ord (Bool, Bool) = EQUAL
+ | mode_ord (Pair (m1, m2), Pair (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
+ | mode_ord (Fun (m1, m2), Fun (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
+
fun list_fun_mode [] = Bool
| list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms)