1.1 --- a/src/Tools/isac/CalcElements/KEStore.thy	Sat Apr 04 12:11:32 2020 +0200
     1.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy	Mon Apr 06 11:44:36 2020 +0200
     1.3 @@ -31,8 +31,8 @@
     1.4  *)
     1.5  signature KESTORE_ELEMS =
     1.6  sig
     1.7 -  val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list
     1.8 -  val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list -> theory -> theory
     1.9 +  val get_rlss: theory -> (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list
    1.10 +  val add_rlss: (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
    1.11    val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
    1.12    val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
    1.13    val get_cas: theory -> Celem.cas_elem list
    1.14 @@ -53,7 +53,7 @@
    1.15    fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
    1.16  
    1.17    structure Data = Theory_Data (
    1.18 -    type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list;
    1.19 +    type T = (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list;
    1.20      val empty = [];
    1.21      val extend = I;
    1.22      val merge = Rule_Set.merge_rlss;
    1.23 @@ -190,11 +190,11 @@
    1.24  
    1.25  section \<open>Functions for checking KEStore_Elems\<close>
    1.26  ML \<open>
    1.27 -fun short_string_of_rls Rule_Set.Erls = "Erls"
    1.28 -  | short_string_of_rls (Rule_Set.Rls {calc, rules, ...}) =
    1.29 +fun short_string_of_rls Rule_Set.Empty = "Erls"
    1.30 +  | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
    1.31      "Rls {#calc = " ^ string_of_int (length calc) ^
    1.32      ", #rules = " ^ string_of_int (length rules) ^ ", ..."
    1.33 -  | short_string_of_rls (Rule_Set.Seq {calc, rules, ...}) =
    1.34 +  | short_string_of_rls (Rule_Set.Seqence {calc, rules, ...}) =
    1.35      "Seq {#calc = " ^ string_of_int (length calc) ^
    1.36      ", #rules = " ^ string_of_int (length rules) ^ ", ..."
    1.37    | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";