1.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml	Wed Sep 20 08:27:21 2023 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml	Wed Sep 20 11:30:50 2023 +0200
     1.3 @@ -38,9 +38,9 @@
     1.4      | Mis of (term * term) 
     1.5      | Par of TermC.as_string
     1.6    datatype i_model_feedback_TEST = 
     1.7 -      Cor_TEST of (descriptor * (term list)) * (term * (term list))
     1.8 +      Cor_TEST of (descriptor * (term list))
     1.9      | Syn_TEST of TermC.as_string 
    1.10 -    | Inc_TEST of (descriptor * (term list)) * (term * (term list))
    1.11 +    | Inc_TEST of (descriptor * (term list))
    1.12      | Sup_TEST of (descriptor * (term list)) 
    1.13    val feedback_empty_TEST: i_model_feedback_TEST
    1.14  
    1.15 @@ -100,13 +100,12 @@
    1.16  *)
    1.17  datatype i_model_feedback_TEST = 
    1.18    Cor_TEST of (descriptor * (* correct input: descriptor, see Input_Descript.thy *)
    1.19 -     (values)) *              (* set of values for list-types: for decdiing
    1.20 +     (values))                (* set of values for list-types: for decding
    1.21                                   Inc the values packed out from the list;
    1.22                                   They are packed back to an isalist for envs     *)
    1.23 -   (term * (term list))       (* will be eliminated in i_model_feedback_TEST     *)
    1.24  | Syn_TEST of TermC.as_string (* syntax error kept for P_Model.switch_pbl_met    *)
    1.25 -| Inc_TEST of (descriptor * values) * (term * (term list))  (* see Cor           *)
    1.26 -| Sup_TEST of (descriptor * values)(* superfluous; input not found in O_Model.T  *)
    1.27 +| Inc_TEST of (descriptor * values) (* see Cor                                   *)
    1.28 +| Sup_TEST of (descriptor * values) (* superfluous; input not found in O_Model.T *)
    1.29  val feedback_empty_TEST = Syn_TEST "i_model_empty"
    1.30  
    1.31