1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Fri May 15 14:22:05 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Fri May 15 19:31:04 2020 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  ML_file "store.sml"
     1.6  ML_file "check-unique.sml"
     1.7 -ML_file "references.sml"
     1.8 +ML_file "references-def.sml"
     1.9  ML_file "model-pattern.sml"
    1.10  ML_file "problem-def.sml"
    1.11  ML_file "method-def.sml"
    1.12 @@ -66,9 +66,9 @@
    1.13    val get_cas: theory -> CAS_Def.T list
    1.14    val add_cas: CAS_Def.T list -> theory -> theory
    1.15    val get_ptyps: theory -> Probl_Def.store
    1.16 -  val add_pbts: (Probl_Def.T * References.id) list -> theory -> theory
    1.17 +  val add_pbts: (Probl_Def.T * References_Def.id) list -> theory -> theory
    1.18    val get_mets: theory -> Meth_Def.store
    1.19 -  val add_mets: (Meth_Def.T * References.id) list -> theory -> theory
    1.20 +  val add_mets: (Meth_Def.T * References_Def.id) list -> theory -> theory
    1.21    val get_thes: theory -> (Thy_Write.thydata Store.node) list
    1.22    val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.23    val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory 
    1.24 @@ -99,7 +99,7 @@
    1.25    fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
    1.26  
    1.27    structure Data = Theory_Data (
    1.28 -    type T = (term * (References.T * (term list -> (term * term list) list))) list;
    1.29 +    type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
    1.30      val empty = [];
    1.31      val extend = I;
    1.32      val merge = merge CAS_Def.equal;
    1.33 @@ -234,7 +234,7 @@
    1.34  (* we avoid term_to_string''' defined later *)
    1.35  fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
    1.36    "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
    1.37 -  (Proof_Context.init_global @{theory})))) t ^ ", " ^ References.to_string s ^ ")";
    1.38 +  (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
    1.39  
    1.40  fun count_kestore_ptyps [] = 0
    1.41    | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =