1.1 --- a/src/Tools/isac/Specify/ptyps.sml	Wed Apr 08 16:56:47 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/ptyps.sml	Thu Apr 09 11:21:53 2020 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4        Celem.pbt * Celem.pblID
     1.5    val prep_met : theory -> string -> string list -> Celem.pblID ->
     1.6       string list * (string * string list) list *
     1.7 -       {calc: 'a, crls: Rule_Set.T, errpats: Rule.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
     1.8 +       {calc: 'a, crls: Rule_Set.T, errpats: Error_Fill_Def.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
     1.9           rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} * thm ->
    1.10       Celem.met * Celem.metID
    1.11  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.12 @@ -55,7 +55,7 @@
    1.13    datatype match' = Matches' of Model.item Model.ppc | NoMatch' of Model.item Model.ppc
    1.14    val match_pbl : Selem.fmz_ -> Celem.pbt -> match'
    1.15    val refine : Selem.fmz_ -> Celem.pblID -> Stool.match list
    1.16 -  val e_errpat : Rule.errpat
    1.17 +  val e_errpat : Error_Fill_Def.errpat
    1.18    val show_pblguhs : unit -> unit
    1.19    val sort_pblguhs : unit -> unit
    1.20  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.21 @@ -275,7 +275,7 @@
    1.22          |> map flattup;
    1.23      in (oris, ctxt) end;
    1.24  
    1.25 -val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Rule.errpat
    1.26 +val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Error_Fill_Def.errpat
    1.27  val e_fillpat = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
    1.28  
    1.29  (** breadth-first search on hierarchy of problem-types **)