1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Wed Sep 20 08:27:21 2023 +0200
     1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy	Wed Sep 20 11:30:50 2023 +0200
     1.3 @@ -38,11 +38,11 @@
     1.4      fun extract (_, _, _, _, itm_) = itm_
     1.5    in map (xml_of_itm_ o extract) itms end
     1.6  (*T_TEST*)
     1.7 -fun xml_of_itm_TEST (I_Model.Cor_TEST (dts, _)) =
     1.8 +fun xml_of_itm_TEST (I_Model.Cor_TEST dts) =
     1.9      XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])
    1.10    | xml_of_itm_TEST (I_Model.Syn_TEST c) =
    1.11      XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
    1.12 -  | xml_of_itm_TEST (I_Model.Inc_TEST (dts, _)) = 
    1.13 +  | xml_of_itm_TEST (I_Model.Inc_TEST dts) = 
    1.14      XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])
    1.15    | xml_of_itm_TEST (I_Model.Sup_TEST dts) = 
    1.16      XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])