src/Sequents/prover.ML
changeset 4440 9ed4098074bc
parent 3948 3428c0a88449
child 6054 4a4f6ad607a1
--- a/src/Sequents/prover.ML	Fri Dec 19 09:58:42 1997 +0100
+++ b/src/Sequents/prover.ML	Fri Dec 19 10:13:47 1997 +0100
@@ -22,10 +22,10 @@
 infix 4 add_safes add_unsafes;
 
 fun (Pack(safes,unsafes)) add_safes ths   = 
-    Pack(sort less (ths@safes), unsafes);
+    Pack(sort (make_ord less) (ths@safes), unsafes);
 
 fun (Pack(safes,unsafes)) add_unsafes ths = 
-    Pack(safes, sort less (ths@unsafes));
+    Pack(safes, sort (make_ord less) (ths@unsafes));
 
 
 (*Returns the list of all formulas in the sequent*)