1.1 --- a/src/Tools/isac/Specify/pre-conditions.sml	Fri Aug 18 18:51:18 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml	Sat Aug 19 05:06:55 2023 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5    val to_string : Proof.context -> T -> string
     1.6  
     1.7 -  val max_variant: Model_Def.i_model -> int
     1.8 +  val max_variant: Model_Def.i_model -> Model_Def.variant
     1.9  (*T_TESTold* )
    1.10    val environment: Model_Def.i_model -> Env.T
    1.11  ( *T_TEST*)
    1.12 @@ -179,8 +179,8 @@
    1.13  fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);
    1.14  fun count_variants vts itms = map (cnt itms) vts;
    1.15  
    1.16 -fun max2 [] = raise ERROR "max2 of []"
    1.17 -  | max2 (y :: ys) =
    1.18 +fun max_list [] = raise ERROR "max_list of []"
    1.19 +  | max_list (y :: ys) =
    1.20      let
    1.21        fun mx (a, x) [] = (a, x)
    1.22    	    | mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
    1.23 @@ -197,10 +197,10 @@
    1.24  	    | _ => (id, v1));
    1.25  ( **)
    1.26  
    1.27 -(* find the variant with most items already input *)
    1.28 +(* find the variant with most items already input, without Pre_Conds (of_max_variant) *)
    1.29  fun max_variant itms = 
    1.30      let val vts = (count_variants (variants itms)) itms;
    1.31 -    in if vts = [] then 0 else (fst o max2) vts end;
    1.32 +    in if vts = [] then 0 else (fst o max_list) vts end;
    1.33  
    1.34  (** )
    1.35  fun mk_e (Cor (_, iv)) = [getval iv]