src/FOLP/intprover.ML

--- a/src/FOLP/intprover.ML	Fri Dec 19 09:58:42 1997 +0100
+++ b/src/FOLP/intprover.ML	Fri Dec 19 10:13:47 1997 +0100
@@ -35,7 +35,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),