1.1 --- a/src/Tools/isac/Specify/pre-conditions.sml	Thu Nov 16 08:15:46 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml	Sun Nov 19 07:51:41 2023 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4    val all_lhs_atoms: term list -> bool
     1.5  (*/------- \<longrightarrow> pre-conditions*)
     1.6    val is_list_descr: Model_Pattern.descriptor -> bool
     1.7 -  val is_NObrack_list: Model_Pattern.descriptor -> Model_Pattern.values -> bool
     1.8 +  val is_NObrack_list: Model_Pattern.descriptor -> bool
     1.9  (*\------- \<longrightarrow> pre-conditions*)
    1.10    val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;
    1.11    val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST
    1.12 @@ -230,9 +230,11 @@
    1.13         (descr = bieg_descr andalso subset op= (values, bieg_values)))
    1.14    end
    1.15  ( *---*)
    1.16 -fun is_NObrack_list descr _ =
    1.17 -  (*HACK: before introduction typedecl toreallNObrack, toboollNObrack*)
    1.18 -  descr = @{term solutions} orelse descr = @{term solution} orelse descr = @{term Gleichungen}
    1.19 +(*HACK: until introduction typedecl toreallNObrack, toboollNObrack*)
    1.20 +fun is_NObrack_list (Const ("Input_Descript.solutions", _)) = true
    1.21 +  | is_NObrack_list (Const ("EqSystem.solution", _)) = true
    1.22 +  | is_NObrack_list (Const ("Biegelinie.Gleichungen", _)) = true
    1.23 +  | is_NObrack_list _ = false
    1.24  
    1.25  fun handle_lists id (descr, ts) =
    1.26    if is_list_descr descr