# HG changeset patch
# User wenzelm
# Date 1128795335 -7200
# Node ID 86daafee72d613d904109cac96518255eca4cad0
# Parent  5b18c334302810a6a525aa312469d91922b835eb
minor tweaks for Poplog/PML;
removed redundant max function;

diff -r 5b18c3343028 -r 86daafee72d6 src/Pure/IsaPlanner/isaplib.ML
--- a/src/Pure/IsaPlanner/isaplib.ML	Sat Oct 08 20:15:34 2005 +0200
+++ b/src/Pure/IsaPlanner/isaplib.ML	Sat Oct 08 20:15:35 2005 +0200
@@ -12,9 +12,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
 signature ISAP_LIB =
 sig
-  (* ints *)
-  val max : int * int -> int
-
   (* seq operations *)
   val ALL_BUT_LAST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
   val FST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
@@ -66,12 +63,9 @@
 
 
 
-structure IsaPLib :> ISAP_LIB = 
+structure IsaPLib : ISAP_LIB = 
 struct
  
-(* Int *)
-fun max (x,y) = if x > y then x else y;
-
 (* Seq *)
 fun seq_map_to_some_filter f s0 =
     let