# HG changeset patch
# User wenzelm
# Date 1128795336 -7200
# Node ID 9996f3a0ffdf5a87a24b30081a485c3c38b66758
# Parent  86daafee72d613d904109cac96518255eca4cad0
Int.max;

diff -r 86daafee72d6 -r 9996f3a0ffdf src/Pure/IsaPlanner/term_lib.ML
--- a/src/Pure/IsaPlanner/term_lib.ML	Sat Oct 08 20:15:35 2005 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML	Sat Oct 08 20:15:36 2005 +0200
@@ -129,12 +129,12 @@
    Note: not stable of eta-contraction: embedding eta-expands term,
    thus we assume eta-expanded *)
 fun fo_term_height (a $ b) =
-    IsaPLib.max (1 + fo_term_height b, (fo_term_height a))
+    Int.max (1 + fo_term_height b, (fo_term_height a))
   | fo_term_height (Abs(_,_,t)) = fo_term_height t
   | fo_term_height _ = 0;
 
 fun ho_term_height  (a $ b) =
-    1 + (IsaPLib.max (ho_term_height b, ho_term_height a))
+    1 + (Int.max (ho_term_height b, ho_term_height a))
   | ho_term_height (Abs(_,_,t)) = ho_term_height t
   | ho_term_height _ = 0;