# 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