1.1 --- a/src/Tools/isac/Interpret/error-pattern.sml	Tue May 12 17:42:29 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml	Wed May 13 11:34:05 2020 +0200
     1.3 @@ -12,9 +12,12 @@
     1.4    type id = Error_Pattern_Def.id
     1.5    type T = Error_Pattern_Def.T
     1.6    val s_to_string : T list -> string
     1.7 +  val empty: T
     1.8  
     1.9    type fill_in_id = Error_Pattern_Def.fill_in_id
    1.10    type fill_in = Error_Pattern_Def.fill_in
    1.11 +  val fill_in_empty: fill_in
    1.12 +
    1.13    type record
    1.14  
    1.15    val from_store: Tactic.input -> Error_Pattern_Def.id list
    1.16 @@ -40,9 +43,12 @@
    1.17  type id = Error_Pattern_Def.id;
    1.18  type T = Error_Pattern_Def.T;
    1.19  val s_to_string = Error_Pattern_Def.s_to_string;
    1.20 +val empty = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}])
    1.21  
    1.22  type fill_in_id = Error_Pattern_Def.fill_in_id;
    1.23  type fill_in = Error_Pattern_Def.fill_in;
    1.24 +val fill_in_empty = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
    1.25 +
    1.26  type record = (fill_in_id * term * thm * Subst.input option);
    1.27  
    1.28  (*