src/FOLP/classical.ML
changeset 4440 9ed4098074bc
parent 1459 d12da312eff4
child 4653 d60f76680bf4
     1.1 --- a/src/FOLP/classical.ML	Fri Dec 19 09:58:42 1997 +0100
     1.2 +++ b/src/FOLP/classical.ML	Fri Dec 19 10:13:47 1997 +0100
     1.3 @@ -113,10 +113,10 @@
     1.4  fun make_cs {safeIs,safeEs,hazIs,hazEs} =
     1.5    let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
     1.6            partition (apl(0,op=) o subgoals_of_brl) 
     1.7 -             (sort lessb (joinrules(safeIs, safeEs)))
     1.8 +             (sort (make_ord lessb) (joinrules(safeIs, safeEs)))
     1.9    in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
    1.10          safe0_brls=safe0_brls, safep_brls=safep_brls,
    1.11 -        haz_brls = sort lessb (joinrules(hazIs, hazEs))}
    1.12 +        haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))}
    1.13    end;
    1.14  
    1.15  (*** Manipulation of clasets ***)