# HG changeset patch
# User wenzelm
# Date 882522827 -3600
# Node ID 9ed4098074bcc346a5225f59b7d22fd49afe4755
# Parent  02730662e4464e1885093866bda501d08a1b158d
adapted to new sort function;

diff -r 02730662e446 -r 9ed4098074bc src/CTT/CTT.ML
--- a/src/CTT/CTT.ML	Fri Dec 19 09:58:42 1997 +0100
+++ b/src/CTT/CTT.ML	Fri Dec 19 10:13:47 1997 +0100
@@ -150,7 +150,7 @@
 fun mp_tac i = etac subst_prodE i  THEN  assume_tac i;
 
 (*"safe" when regarded as predicate calculus rules*)
-val safe_brls = sort lessb 
+val safe_brls = sort (make_ord lessb)
     [ (true,FE), (true,asm_rl), 
       (false,ProdI), (true,SumE), (true,PlusE) ];
 
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),
diff -r 02730662e446 -r 9ed4098074bc src/FOLP/classical.ML
--- a/src/FOLP/classical.ML	Fri Dec 19 09:58:42 1997 +0100
+++ b/src/FOLP/classical.ML	Fri Dec 19 10:13:47 1997 +0100
@@ -113,10 +113,10 @@
 fun make_cs {safeIs,safeEs,hazIs,hazEs} =
   let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
           partition (apl(0,op=) o subgoals_of_brl) 
-             (sort lessb (joinrules(safeIs, safeEs)))
+             (sort (make_ord lessb) (joinrules(safeIs, safeEs)))
   in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
         safe0_brls=safe0_brls, safep_brls=safep_brls,
-        haz_brls = sort lessb (joinrules(hazIs, hazEs))}
+        haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))}
   end;
 
 (*** Manipulation of clasets ***)
diff -r 02730662e446 -r 9ed4098074bc 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),
diff -r 02730662e446 -r 9ed4098074bc src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Dec 19 09:58:42 1997 +0100
+++ b/src/Pure/display.ML	Fri Dec 19 10:13:47 1997 +0100
@@ -147,7 +147,7 @@
       [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
 
     val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
-    val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
+    val spaces' = sort_wrt fst spaces;
     val {classes, classrel, default, tycons, abbrs, arities} =
       Type.rep_tsig tsig;
     val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab));
@@ -219,10 +219,8 @@
     | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
     | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
 
-  fun less_idx ((x, i):indexname, (y, j):indexname) =
-    x < y orelse x = y andalso i < j;
-  fun sort_idxs l = map (apsnd (sort less_idx)) l;
-  fun sort_cnsts l = map (apsnd (sort_wrt fst)) l;
+  fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
+  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
 
 
   (* prepare atoms *)
diff -r 02730662e446 -r 9ed4098074bc src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Dec 19 09:58:42 1997 +0100
+++ b/src/Pure/drule.ML	Fri Dec 19 10:13:47 1997 +0100
@@ -215,7 +215,7 @@
 fun forall_intr_frees th =
     let val {prop,sign,...} = rep_thm th
     in  forall_intr_list
-         (map (cterm_of sign) (sort atless (term_frees prop)))
+         (map (cterm_of sign) (sort (make_ord atless) (term_frees prop)))
          th
     end;
 
diff -r 02730662e446 -r 9ed4098074bc src/Sequents/prover.ML
--- 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*)