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*)