1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Apr 22 11:23:30 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Apr 22 14:36:27 2020 +0200
     1.3 @@ -66,9 +66,9 @@
     1.4    val get_cas: theory -> CAS_Def.T list
     1.5    val add_cas: CAS_Def.T list -> theory -> theory
     1.6    val get_ptyps: theory -> Probl_Def.store
     1.7 -  val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
     1.8 +  val add_pbts: (Probl_Def.T * Spec.id) list -> theory -> theory
     1.9    val get_mets: theory -> Meth_Def.store
    1.10 -  val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory
    1.11 +  val add_mets: (Meth_Def.T * Spec.id) list -> theory -> theory
    1.12    val get_thes: theory -> (Thy_Html.thydata Store.node) list
    1.13    val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.14    val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
    1.15 @@ -99,7 +99,7 @@
    1.16    fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
    1.17  
    1.18    structure Data = Theory_Data (
    1.19 -    type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
    1.20 +    type T = (term * (Spec.T * (term list -> (term * term list) list))) list;
    1.21      val empty = [];
    1.22      val extend = I;
    1.23      val merge = merge CAS_Def.equal;