1.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml	Fri Jul 14 10:15:38 2023 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml	Fri Jul 14 12:33:25 2023 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4      | Proper of (m_field * (descriptor * term) * Position.T)
     1.5    val parse_pattern: Proof.context -> 'a * (string * Position.T) -> 'a * term * Position.T
     1.6  
     1.7 +  val typ_of_element: descriptor -> typ
     1.8    val is_list_descr: descriptor -> bool
     1.9    val empty_for: descriptor -> empty_input
    1.10    val parse_term: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) ->
    1.11 @@ -75,6 +76,10 @@
    1.12  fun descr_type (Type ("fun", [Type ("List.list", [typ]), _])) = List typ
    1.13    | descr_type (Type ("fun", [typ, _])) = Single typ
    1.14    | descr_type typ = raise TYPE ("Model_Pattern.descr_type", [typ], [])
    1.15 +fun typ_of_element descr =
    1.16 +  case descr_type (type_of descr) of
    1.17 +    List typ => typ
    1.18 +  | Single typ => typ
    1.19  fun is_list_descr descr =
    1.20    case descr_type (type_of descr) of List _ => true | _ => false
    1.21  fun empty_for descr =