1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 16:17:27 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sun Apr 19 16:43:53 2020 +0200
     1.3 @@ -30,9 +30,8 @@
     1.4  ML_file "rule-set.sml"
     1.5  
     1.6  ML_file "celem-0.sml"  (*survey Celem.*)
     1.7 -ML_file "celem-1.sml"  (*datatype 'a ptyp*)
     1.8 -ML_file "celem-2.sml"  (*guh*)
     1.9 -ML_file "celem-3.sml"  (*spec*)
    1.10 +ML_file "store.sml"
    1.11 +ML_file "specification.sml"
    1.12  ML_file "celem-4.sml"  (*pat*)
    1.13  ML_file "celem-5.sml"  (*ptyps*)
    1.14  ML_file "celem-6.sml"  (*mets*)
    1.15 @@ -69,9 +68,9 @@
    1.16    val get_cas: theory -> Celem7.cas_elem list
    1.17    val add_cas: Celem7.cas_elem list -> theory -> theory
    1.18    val get_ptyps: theory -> Celem5.ptyps
    1.19 -  val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
    1.20 +  val add_pbts: (Celem5.pbt * Spec.pblID) list -> theory -> theory
    1.21    val get_mets: theory -> Celem6.mets
    1.22 -  val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
    1.23 +  val add_mets: (Celem6.met * Spec.metID) list -> theory -> theory
    1.24    val get_thes: theory -> (Celem8.thydata Store.ptyp) list
    1.25    val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
    1.26    val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory 
    1.27 @@ -102,7 +101,7 @@
    1.28    fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
    1.29  
    1.30    structure Data = Theory_Data (
    1.31 -    type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list;
    1.32 +    type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
    1.33      val empty = [];
    1.34      val extend = I;
    1.35      val merge = merge Celem7.cas_eq;
    1.36 @@ -237,7 +236,7 @@
    1.37  (* we avoid term_to_string''' defined later *)
    1.38  fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
    1.39    "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
    1.40 -  (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
    1.41 +  (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
    1.42  
    1.43  fun count_kestore_ptyps [] = 0
    1.44    | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =