author wenzelm Fri Dec 19 10:13:47 1997 +0100 (1997-12-19) changeset 4440 9ed4098074bc parent 4439 02730662e446 child 4441 42cdcacb60e2
adapted to new sort function;
 src/CTT/CTT.ML file | annotate | diff | revisions src/FOL/intprover.ML file | annotate | diff | revisions src/FOLP/classical.ML file | annotate | diff | revisions src/FOLP/intprover.ML file | annotate | diff | revisions src/Pure/display.ML file | annotate | diff | revisions src/Pure/drule.ML file | annotate | diff | revisions src/Sequents/prover.ML file | annotate | diff | revisions
```     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 @@