206 ML \<open> |
206 ML \<open> |
207 fun short_string_of_rls Rule_Set.Empty = "Erls" |
207 fun short_string_of_rls Rule_Set.Empty = "Erls" |
208 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) = |
208 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) = |
209 "Rls {#calc = " ^ string_of_int (length calc) ^ |
209 "Rls {#calc = " ^ string_of_int (length calc) ^ |
210 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
210 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
211 | short_string_of_rls (Rule_Set.Seqence {calc, rules, ...}) = |
211 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) = |
212 "Seq {#calc = " ^ string_of_int (length calc) ^ |
212 "Seq {#calc = " ^ string_of_int (length calc) ^ |
213 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
213 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
214 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}"; |
214 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}"; |
215 fun check_kestore_rls (rls', (thyID, rls)) = |
215 fun check_kestore_rls (rls', (thyID, rls)) = |
216 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))"; |
216 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))"; |