src/Tools/isac/BaseDefinitions/Know_Store.thy
changeset 59909 821f038df564
parent 59904 2e0fa83971e5
child 59917 e98d714cca1a
     1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Thu Apr 23 15:48:31 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Fri Apr 24 08:51:05 2020 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  ML_file "exec-def.sml"       (*rename identifiers by use of struct.id*)
     1.5  ML_file "rewrite-order.sml"  (*rename identifiers by use of struct.id*)
     1.6  ML_file rule.sml
     1.7 -ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
     1.8 +ML_file "error-pattern-def.sml"
     1.9  ML_file "rule-set.sml"
    1.10  
    1.11  ML_file "store.sml"
    1.12 @@ -71,7 +71,7 @@
    1.13    val add_mets: (Meth_Def.T * Spec.id) list -> theory -> theory
    1.14    val get_thes: theory -> (Thy_Html.thydata Store.node) list
    1.15    val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.16 -  val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
    1.17 +  val insert_fillpats: (Thy_Html.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory 
    1.18    val get_ref_thy: unit -> theory
    1.19    val set_ref_thy: theory -> unit
    1.20  end;