1.1 --- a/src/Tools/isac/BaseDefinitions/error-pattern-def.sml	Mon Sep 26 10:57:53 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/error-pattern-def.sml	Thu Sep 29 18:02:10 2022 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    eqtype id
     1.5    type T = id * term list * thm list
     1.6    val s_to_string : T list -> string
     1.7 +  val adapt_to_type: Proof.context -> T -> T
     1.8  
     1.9    type fill_in_id
    1.10    type fill_in
    1.11 @@ -32,6 +33,9 @@
    1.12    "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms
    1.13  fun s_to_string errpats = (strs2str' o (map errpat2str)) errpats
    1.14  
    1.15 +fun adapt_to_type ctxt (id, terms, thms) =
    1.16 +  (id, map (Model_Pattern.adapt_term_to_type ctxt) terms, thms)
    1.17 +
    1.18  (* for (at least) 2 kinds of access:
    1.19    (1) given an id, find the respective fill_in's (e.g. in fun find_fill_patterns)
    1.20    (2) given a thm, find respective fill_in's *)