adapted to new sort function;
authorwenzelm
Wed Jan 07 13:55:29 1998 +0100 (1998-01-07)
changeset 4519055f2067d373
parent 4518 74c01296e818
child 4520 d430a1b34928
adapted to new sort function;
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Wed Jan 07 13:53:42 1998 +0100
     1.2 +++ b/src/Provers/splitter.ML	Wed Jan 07 13:55:29 1998 +0100
     1.3 @@ -171,31 +171,20 @@
     1.4  fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
     1.5  
     1.6  fun shorter((_,ps,pos,_,_),(_,qs,qos,_,_)) =
     1.7 -  let val ms = length ps and ns = length qs
     1.8 -  in ms < ns orelse (ms = ns andalso order(length pos,length qos)) end;
     1.9 +  prod_ord (int_ord o pairself length) (order o pairself length)
    1.10 +    ((ps, pos), (qs, qos));
    1.11 +
    1.12  
    1.13  
    1.14  (************************************************************
    1.15     call split_posns with appropriate parameters
    1.16  *************************************************************)
    1.17  
    1.18 -(* FIXME *)
    1.19 -(*insertion sort; stable (does not reorder equal elements)
    1.20 -  'less' is less-than test on type 'a*)
    1.21 -fun sort (less: 'a*'a -> bool) =
    1.22 -  let fun insert (x, []) = [x]
    1.23 -        | insert (x, y::ys) =
    1.24 -              if less(y, x) then y :: insert (x, ys) else x::y::ys;
    1.25 -      fun sort1 [] = []
    1.26 -        | sort1 (x::xs) = insert (x, sort1 xs)
    1.27 -  in  sort1  end;
    1.28 -
    1.29 -
    1.30  fun select cmap state i =
    1.31    let val goali = nth_subgoal i state
    1.32        val Ts = rev(map #2 (Logic.strip_params goali))
    1.33        val _ $ t $ _ = Logic.strip_assums_concl goali;
    1.34 -  in (Ts,t,sort shorter (split_posns cmap Ts t)) end;
    1.35 +  in (Ts,t, sort shorter (split_posns cmap Ts t)) end;
    1.36  
    1.37  
    1.38  (*************************************************************
    1.39 @@ -341,9 +330,9 @@
    1.40  
    1.41  in
    1.42  
    1.43 -fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD (op <=) ;
    1.44 +fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD int_ord;
    1.45  
    1.46 -fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (op >=) ;
    1.47 +fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (rev_order o int_ord);
    1.48  
    1.49  val mk_case_split_asm_tac = mk_case_split_asm_tac;
    1.50