1.1 --- a/src/Tools/isac/Specify/i-model.sml	Tue Aug 15 17:44:56 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Thu Aug 17 08:01:45 2023 +0200
     1.3 @@ -66,8 +66,10 @@
     1.4    val to_p_model: theory -> feedback -> string
     1.5    val eq1: ''a -> 'b * (''a * 'c) -> bool
     1.6  
     1.7 +(** )
     1.8    val is_complete_OLD: Proof.context -> Model_Pattern.T -> Rule_Def.rule_set ->
     1.9      Pre_Conds.unchecked -> T_TEST -> variants option
    1.10 +( **)
    1.11    val is_complete_variant: int -> T_TEST-> bool
    1.12  
    1.13  (*T_TESTold* )
    1.14 @@ -508,6 +510,7 @@
    1.15  fun is_complete_variant no_model_items i_model =
    1.16    no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) =>  true | _ => false) i_model)
    1.17  
    1.18 +(** )
    1.19  fun is_complete_OLD ctxt model_patt where_rls pres i_model =
    1.20    let
    1.21      val no_model_items = length model_patt
    1.22 @@ -522,6 +525,7 @@
    1.23      then NONE
    1.24      else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
    1.25    end
    1.26 +( **)
    1.27  
    1.28  val of_max_variant = Pre_Conds.of_max_variant
    1.29