diff -r 02730662e446 -r 9ed4098074bc src/FOL/intprover.ML
--- a/src/FOL/intprover.ML	Fri Dec 19 09:58:42 1997 +0100
+++ b/src/FOL/intprover.ML	Fri Dec 19 10:13:47 1997 +0100
@@ -37,7 +37,7 @@
   (handles double negations).  Could instead rewrite by not_def as the first
   step of an intuitionistic proof.
 *)
-val safe_brls = sort lessb 
+val safe_brls = sort (make_ord lessb)
     [ (true,FalseE), (false,TrueI), (false,refl),
       (false,impI), (false,notI), (false,allI),
       (true,conjE), (true,exE),