diff -r df8636ffd6f8 -r 41abd196342a src/Tools/isac/Specify/pre-conditions.sml
--- a/src/Tools/isac/Specify/pre-conditions.sml	Sun Dec 10 17:35:07 2023 +0100
+++ b/src/Tools/isac/Specify/pre-conditions.sml	Mon Dec 11 09:24:02 2023 +0100
@@ -18,9 +18,7 @@
   val to_string : Proof.context -> T -> string
   val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
 
-  val max_variant: Model_Def.i_model -> Model_Def.variant
   val environment_POS: Model_Pattern.T -> Model_Def.i_model_POS -> Env.T
-
   val make_environments: Model_Pattern.T -> Model_Def.i_model_POS -> Env.T * (env_subst * env_eval)
   val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_POS) list ->
     ((term * term) * (term * term)) list
@@ -117,26 +115,6 @@
 
 (** find the maximal variant within an I_Model.T **)
 
-(* old code before I_Model.T_POS *)
-(*ATTENTION: misses variants with equal number of items, etc*)
-fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);
-fun count_variants vts itms = map (cnt itms) vts;
-
-fun max_list [] = raise ERROR "max_list of []"
-  | max_list (y :: ys) =
-    let
-      fun mx (a, x) [] = (a, x)             
-  	    | mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
-    in mx y ys end;
-
-(*find most frequent variant v in itms*)
-fun variants itms = ((distinct op =) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms;
-(*find the variant with most items already input, without Pre_Conds (make_environments)*)
-(*T_POSold \<rightarrow> fun max_variants*)
-fun max_variant itms = 
-    let val vts = (count_variants (variants itms)) itms;
-    in if vts = [] then 0 else (fst o max_list) vts end;
-
 fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =
   let
     val equal_descr =