adapted to new sort function;
authorwenzelm
Fri Dec 19 10:13:47 1997 +0100 (1997-12-19)
changeset 44409ed4098074bc
parent 4439 02730662e446
child 4441 42cdcacb60e2
adapted to new sort function;
src/CTT/CTT.ML
src/FOL/intprover.ML
src/FOLP/classical.ML
src/FOLP/intprover.ML
src/Pure/display.ML
src/Pure/drule.ML
src/Sequents/prover.ML
     1.1 --- a/src/CTT/CTT.ML	Fri Dec 19 09:58:42 1997 +0100
     1.2 +++ b/src/CTT/CTT.ML	Fri Dec 19 10:13:47 1997 +0100
     1.3 @@ -150,7 +150,7 @@
     1.4  fun mp_tac i = etac subst_prodE i  THEN  assume_tac i;
     1.5  
     1.6  (*"safe" when regarded as predicate calculus rules*)
     1.7 -val safe_brls = sort lessb 
     1.8 +val safe_brls = sort (make_ord lessb)
     1.9      [ (true,FE), (true,asm_rl), 
    1.10        (false,ProdI), (true,SumE), (true,PlusE) ];
    1.11  
     2.1 --- a/src/FOL/intprover.ML	Fri Dec 19 09:58:42 1997 +0100
     2.2 +++ b/src/FOL/intprover.ML	Fri Dec 19 10:13:47 1997 +0100
     2.3 @@ -37,7 +37,7 @@
     2.4    (handles double negations).  Could instead rewrite by not_def as the first
     2.5    step of an intuitionistic proof.
     2.6  *)
     2.7 -val safe_brls = sort lessb 
     2.8 +val safe_brls = sort (make_ord lessb)
     2.9      [ (true,FalseE), (false,TrueI), (false,refl),
    2.10        (false,impI), (false,notI), (false,allI),
    2.11        (true,conjE), (true,exE),
     3.1 --- a/src/FOLP/classical.ML	Fri Dec 19 09:58:42 1997 +0100
     3.2 +++ b/src/FOLP/classical.ML	Fri Dec 19 10:13:47 1997 +0100
     3.3 @@ -113,10 +113,10 @@
     3.4  fun make_cs {safeIs,safeEs,hazIs,hazEs} =
     3.5    let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
     3.6            partition (apl(0,op=) o subgoals_of_brl) 
     3.7 -             (sort lessb (joinrules(safeIs, safeEs)))
     3.8 +             (sort (make_ord lessb) (joinrules(safeIs, safeEs)))
     3.9    in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
    3.10          safe0_brls=safe0_brls, safep_brls=safep_brls,
    3.11 -        haz_brls = sort lessb (joinrules(hazIs, hazEs))}
    3.12 +        haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))}
    3.13    end;
    3.14  
    3.15  (*** Manipulation of clasets ***)
     4.1 --- a/src/FOLP/intprover.ML	Fri Dec 19 09:58:42 1997 +0100
     4.2 +++ b/src/FOLP/intprover.ML	Fri Dec 19 10:13:47 1997 +0100
     4.3 @@ -35,7 +35,7 @@
     4.4    (handles double negations).  Could instead rewrite by not_def as the first
     4.5    step of an intuitionistic proof.
     4.6  *)
     4.7 -val safe_brls = sort lessb 
     4.8 +val safe_brls = sort (make_ord lessb)
     4.9      [ (true,FalseE), (false,TrueI), (false,refl),
    4.10        (false,impI), (false,notI), (false,allI),
    4.11        (true,conjE), (true,exE),
     5.1 --- a/src/Pure/display.ML	Fri Dec 19 09:58:42 1997 +0100
     5.2 +++ b/src/Pure/display.ML	Fri Dec 19 10:13:47 1997 +0100
     5.3 @@ -147,7 +147,7 @@
     5.4        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
     5.5  
     5.6      val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
     5.7 -    val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
     5.8 +    val spaces' = sort_wrt fst spaces;
     5.9      val {classes, classrel, default, tycons, abbrs, arities} =
    5.10        Type.rep_tsig tsig;
    5.11      val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab));
    5.12 @@ -219,10 +219,8 @@
    5.13      | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
    5.14      | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
    5.15  
    5.16 -  fun less_idx ((x, i):indexname, (y, j):indexname) =
    5.17 -    x < y orelse x = y andalso i < j;
    5.18 -  fun sort_idxs l = map (apsnd (sort less_idx)) l;
    5.19 -  fun sort_cnsts l = map (apsnd (sort_wrt fst)) l;
    5.20 +  fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    5.21 +  fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    5.22  
    5.23  
    5.24    (* prepare atoms *)
     6.1 --- a/src/Pure/drule.ML	Fri Dec 19 09:58:42 1997 +0100
     6.2 +++ b/src/Pure/drule.ML	Fri Dec 19 10:13:47 1997 +0100
     6.3 @@ -215,7 +215,7 @@
     6.4  fun forall_intr_frees th =
     6.5      let val {prop,sign,...} = rep_thm th
     6.6      in  forall_intr_list
     6.7 -         (map (cterm_of sign) (sort atless (term_frees prop)))
     6.8 +         (map (cterm_of sign) (sort (make_ord atless) (term_frees prop)))
     6.9           th
    6.10      end;
    6.11  
     7.1 --- a/src/Sequents/prover.ML	Fri Dec 19 09:58:42 1997 +0100
     7.2 +++ b/src/Sequents/prover.ML	Fri Dec 19 10:13:47 1997 +0100
     7.3 @@ -22,10 +22,10 @@
     7.4  infix 4 add_safes add_unsafes;
     7.5  
     7.6  fun (Pack(safes,unsafes)) add_safes ths   = 
     7.7 -    Pack(sort less (ths@safes), unsafes);
     7.8 +    Pack(sort (make_ord less) (ths@safes), unsafes);
     7.9  
    7.10  fun (Pack(safes,unsafes)) add_unsafes ths = 
    7.11 -    Pack(safes, sort less (ths@unsafes));
    7.12 +    Pack(safes, sort (make_ord less) (ths@unsafes));
    7.13  
    7.14  
    7.15  (*Returns the list of all formulas in the sequent*)