1.1 --- a/src/Tools/isac/Specify/o-model.sml	Fri Aug 18 18:51:18 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/o-model.sml	Sat Aug 19 05:06:55 2023 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values
     1.5  
     1.6    val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
     1.7 -  val max_variant: variants -> int
     1.8 +  val get_max_variant: variants -> variant
     1.9    val partition_variants: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
    1.10    val collect_variants: ('a * ''b) list -> ('a list * ''b) list
    1.11  
    1.12 @@ -137,8 +137,8 @@
    1.13      fun eq (a, b) = curry op= (snd3 a) (snd3 b);
    1.14    in partition_variants eq fdts end;
    1.15  
    1.16 -fun max_variant [] = raise ERROR "max_variant of []"
    1.17 -  | max_variant (y :: ys) =
    1.18 +fun get_max_variant [] = raise ERROR "get_max_variant of []"
    1.19 +  | get_max_variant (y :: ys) =
    1.20    let fun mx x [] = x
    1.21  	| mx x (y :: ys) = if x < y then mx y ys else mx x ys;
    1.22  in mx y ys end;
    1.23 @@ -173,7 +173,7 @@
    1.24            |> Input_Descript.split
    1.25            |> add_field thy pbt) ts)
    1.26          |> add_variants;
    1.27 -      val maxv = model |> map fst |> max_variant;
    1.28 +      val maxv = model |> map fst |> get_max_variant;
    1.29        val maxv = if maxv = 0 then 1 else maxv;
    1.30        val model' = model
    1.31          |> collect_variants

     2.1 --- a/src/Tools/isac/Specify/pre-conditions.sml	Fri Aug 18 18:51:18 2023 +0200
     2.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml	Sat Aug 19 05:06:55 2023 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4  
     2.5    val to_string : Proof.context -> T -> string
     2.6  
     2.7 -  val max_variant: Model_Def.i_model -> int
     2.8 +  val max_variant: Model_Def.i_model -> Model_Def.variant
     2.9  (*T_TESTold* )
    2.10    val environment: Model_Def.i_model -> Env.T
    2.11  ( *T_TEST*)
    2.12 @@ -179,8 +179,8 @@
    2.13  fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);
    2.14  fun count_variants vts itms = map (cnt itms) vts;
    2.15  
    2.16 -fun max2 [] = raise ERROR "max2 of []"
    2.17 -  | max2 (y :: ys) =
    2.18 +fun max_list [] = raise ERROR "max_list of []"
    2.19 +  | max_list (y :: ys) =
    2.20      let
    2.21        fun mx (a, x) [] = (a, x)
    2.22    	    | mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
    2.23 @@ -197,10 +197,10 @@
    2.24  	    | _ => (id, v1));
    2.25  ( **)
    2.26  
    2.27 -(* find the variant with most items already input *)
    2.28 +(* find the variant with most items already input, without Pre_Conds (of_max_variant) *)
    2.29  fun max_variant itms = 
    2.30      let val vts = (count_variants (variants itms)) itms;
    2.31 -    in if vts = [] then 0 else (fst o max2) vts end;
    2.32 +    in if vts = [] then 0 else (fst o max_list) vts end;
    2.33  
    2.34  (** )
    2.35  fun mk_e (Cor (_, iv)) = [getval iv]

     3.1 --- a/test/Tools/isac/Specify/o-model.sml	Fri Aug 18 18:51:18 2023 +0200
     3.2 +++ b/test/Tools/isac/Specify/o-model.sml	Sat Aug 19 05:06:55 2023 +0200
     3.3 @@ -81,7 +81,7 @@
     3.4  (*+*)val eee as [(0, ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)])),
     3.5                   _, _, _, _, _, _] = add_variants ddd;
     3.6  
     3.7 -      val maxv = map fst ori |> max_variant;
     3.8 +      val maxv = map fst ori |> get_max_variant;
     3.9        val maxv = if maxv = 0 then 1 else maxv;
    3.10        val oris = ori
    3.11          |> O_Model.collect_variants

     4.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Fri Aug 18 18:51:18 2023 +0200
     4.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sat Aug 19 05:06:55 2023 +0200
     4.3 @@ -272,11 +272,6 @@
     4.4    ML_file "Interpret/istate.sml"
     4.5    ML_file "Interpret/error-pattern.sml"
     4.6    ML_file "Interpret/li-tool.sml"
     4.7 -ML \<open>
     4.8 -\<close> ML \<open>
     4.9 -
    4.10 -\<close> ML \<open>
    4.11 -\<close>
    4.12    ML_file "Interpret/lucas-interpreter.sml"
    4.13    ML_file "Interpret/step-solve.sml"
    4.14  

     5.1 --- a/test/Tools/isac/Test_Theory.thy	Fri Aug 18 18:51:18 2023 +0200
     5.2 +++ b/test/Tools/isac/Test_Theory.thy	Sat Aug 19 05:06:55 2023 +0200
     5.3 @@ -44,12 +44,12 @@
     5.4    declare [[show_sorts]]
     5.5    find_theorems "?a <= ?a"
     5.6    
     5.7 -  print_theorems
     5.8 +  print_theorems                                    
     5.9    print_facts
    5.10    print_statement ""
    5.11    print_theory
    5.12    ML_command \<open>Pretty.writeln prt\<close>
    5.13 -  declare [[ML_print_depth = 999]]
    5.14 +  declare [[ML_print_depth = 999]]                 
    5.15    declare [[ML_exception_trace]]
    5.16  \<close>
    5.17