1.1 --- a/src/Tools/isac/Specify/pre-conditions.sml	Sun Dec 10 17:35:07 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml	Mon Dec 11 09:24:02 2023 +0100
     1.3 @@ -18,9 +18,7 @@
     1.4    val to_string : Proof.context -> T -> string
     1.5    val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
     1.6  
     1.7 -  val max_variant: Model_Def.i_model -> Model_Def.variant
     1.8    val environment_POS: Model_Pattern.T -> Model_Def.i_model_POS -> Env.T
     1.9 -
    1.10    val make_environments: Model_Pattern.T -> Model_Def.i_model_POS -> Env.T * (env_subst * env_eval)
    1.11    val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_POS) list ->
    1.12      ((term * term) * (term * term)) list
    1.13 @@ -117,26 +115,6 @@
    1.14  
    1.15  (** find the maximal variant within an I_Model.T **)
    1.16  
    1.17 -(* old code before I_Model.T_POS *)
    1.18 -(*ATTENTION: misses variants with equal number of items, etc*)
    1.19 -fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);
    1.20 -fun count_variants vts itms = map (cnt itms) vts;
    1.21 -
    1.22 -fun max_list [] = raise ERROR "max_list of []"
    1.23 -  | max_list (y :: ys) =
    1.24 -    let
    1.25 -      fun mx (a, x) [] = (a, x)             
    1.26 -  	    | mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
    1.27 -    in mx y ys end;
    1.28 -
    1.29 -(*find most frequent variant v in itms*)
    1.30 -fun variants itms = ((distinct op =) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms;
    1.31 -(*find the variant with most items already input, without Pre_Conds (make_environments)*)
    1.32 -(*T_POSold \<rightarrow> fun max_variants*)
    1.33 -fun max_variant itms = 
    1.34 -    let val vts = (count_variants (variants itms)) itms;
    1.35 -    in if vts = [] then 0 else (fst o max_list) vts end;
    1.36 -
    1.37  fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =
    1.38    let
    1.39      val equal_descr =