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