1.1 --- a/src/Tools/isac/Interpret/inform.sml Tue Mar 13 15:04:27 2018 +0100
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Mar 15 10:17:44 2018 +0100
1.3 @@ -6,13 +6,13 @@
1.4
1.5 signature INPUT_FORMULAS =
1.6 sig
1.7 - datatype iitem = Find of cterm' list | Given of cterm' list | Relate of cterm' list
1.8 + datatype iitem = Find of Celem.cterm' list | Given of Celem.cterm' list | Relate of Celem.cterm' list
1.9 type imodel = iitem list
1.10 - type icalhd = Ctree.pos' * cterm' * imodel * Ctree.pos_ * spec
1.11 - val fetchErrorpatterns : Tac.tac -> errpatID list
1.12 + type icalhd = Ctree.pos' * Celem.cterm' * imodel * Ctree.pos_ * Celem.spec
1.13 + val fetchErrorpatterns : Tac.tac -> Celem.errpatID list
1.14 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
1.15 val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
1.16 - val find_fillpatterns : Ctree.state -> errpatID -> (fillpatID * term * thm * Selem.subs option) list
1.17 + val find_fillpatterns : Ctree.state -> Celem.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
1.18 val is_exactly_equal : Ctree.state -> string -> string * Tac.tac
1.19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.20 (* NONE *)
1.21 @@ -45,40 +45,40 @@
1.22 (*** handle an input calc-head ***)
1.23
1.24 datatype iitem =
1.25 - Given of cterm' list
1.26 + Given of Celem.cterm' list
1.27 (*Where is never input*)
1.28 -| Find of cterm' list
1.29 -| Relate of cterm' list
1.30 +| Find of Celem.cterm' list
1.31 +| Relate of Celem.cterm' list
1.32
1.33 type imodel = iitem list
1.34
1.35 (*calc-head as input*)
1.36 type icalhd =
1.37 Ctree.pos' * (*the position of the calc-head in the calc-tree*)
1.38 - cterm' * (*the headline*)
1.39 - imodel * (*the model (without Find) of the calc-head*)
1.40 + Celem.cterm' * (*the headline*)
1.41 + imodel * (*the model (without Find) of the calc-head*)
1.42 Ctree.pos_ * (*model belongs to Pbl or Met*)
1.43 - spec; (*specification: domID, pblID, metID*)
1.44 -val e_icalhd = (Ctree.e_pos', "", [Given [""]], Ctree.Pbl, e_spec) : icalhd
1.45 + Celem.spec; (*specification: domID, pblID, metID*)
1.46 +val e_icalhd = (Ctree.e_pos', "", [Given [""]], Ctree.Pbl, Celem.e_spec)
1.47
1.48 -fun is_casinput (hdf : cterm') ((fmz_, spec) : Selem.fmz) =
1.49 - hdf <> "" andalso fmz_ = [] andalso spec = e_spec
1.50 +fun is_casinput (hdf : Celem.cterm') ((fmz_, spec) : Selem.fmz) =
1.51 + hdf <> "" andalso fmz_ = [] andalso spec = Celem.e_spec
1.52
1.53 (*.handle an input as into an algebra system.*)
1.54 fun dtss2itm_ ppc (d, ts) =
1.55 let
1.56 val (f, (d, id)) = the (find_first ((curry op= d) o
1.57 (#1: (term * term) -> term) o
1.58 - (#2: pbt_ -> (term * term))) ppc)
1.59 + (#2: Celem.pbt_ -> (term * term))) ppc)
1.60 in
1.61 ([1], true, f, Model.Cor ((d, ts), (id, ts)))
1.62 end
1.63
1.64 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
1.65
1.66 -fun cas_input_ ((dI, pI, mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
1.67 +fun cas_input_ ((dI, pI, mI): Celem.spec) dtss = (*WN110515 reconsider thy..ctxt*)
1.68 let
1.69 - val thy = assoc_thy dI
1.70 + val thy = Celem.assoc_thy dI
1.71 val {ppc, ...} = Specify.get_pbt pI
1.72 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.73 val its = Specify.add_id its_
1.74 @@ -104,7 +104,7 @@
1.75 let
1.76 val (h, argl) = strip_comb hdt
1.77 in
1.78 - case assoc_cas (assoc_thy "Isac") h of
1.79 + case assoc_cas (Celem.assoc_thy "Isac") h of
1.80 NONE => NONE
1.81 | SOME (spec as (dI,_,_), argl2dtss) =>
1.82 let
1.83 @@ -112,7 +112,7 @@
1.84 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
1.85 val spec = (dI, pI, mI)
1.86 val (pt,_) =
1.87 - Ctree.cappend_problem Ctree.e_ctree [] (Selem.e_istate, Selem.e_ctxt) ([], e_spec) ([], e_spec, hdt)
1.88 + Ctree.cappend_problem Ctree.e_ctree [] (Selem.e_istate, Selem.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, hdt)
1.89 val pt = Ctree.update_spec pt [] spec
1.90 val pt = Ctree.update_pbl pt [] pits
1.91 val pt = Ctree.update_met pt [] mits
1.92 @@ -123,15 +123,15 @@
1.93 end
1.94
1.95 (*lazy evaluation for (Thy_Info_get_theory "Isac")*)
1.96 -fun Isac _ = assoc_thy "Isac";
1.97 +fun Isac _ = Celem.assoc_thy "Isac";
1.98
1.99 (* re-parse itms with a new thy and prepare for checking with ori list *)
1.100 fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) =
1.101 (let val t = Model.comp_dts (d, ts)
1.102 - val _ = (term_to_string''' dI t)
1.103 + val _ = (Celem.term_to_string''' dI t)
1.104 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
1.105 in itm end
1.106 - handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*))))
1.107 + handle _ => (i, v, false, f, Model.Syn (Celem.term2str Celem.e_term (*t ..(t) has not been declared*))))
1.108 | parsitm dI (i, v, b, f, Model.Syn str) =
1.109 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
1.110 in (i, v, b ,f, Model.Par str) end
1.111 @@ -142,24 +142,24 @@
1.112 handle _ => (i, v, b, f, Model.Syn str))
1.113 | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) =
1.114 (let val t = Model.comp_dts (d,ts);
1.115 - val _ = term_to_string''' dI t;
1.116 + val _ = Celem.term_to_string''' dI t;
1.117 (*this ^ should raise the exn on unability of re-parsing dts*)
1.118 in itm end
1.119 - handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*))))
1.120 + handle _ => (i, v, false, f, Model.Syn (Celem.term2str Celem.e_term (*t ..(t) has not been declared*))))
1.121 | parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) =
1.122 (let val t = Model.comp_dts (d,ts);
1.123 - val _ = term_to_string''' dI t;
1.124 + val _ = Celem.term_to_string''' dI t;
1.125 (*this ^ should raise the exn on unability of re-parsing dts*)
1.126 in itm end
1.127 - handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*))))
1.128 + handle _ => (i, v, false, f, Model.Syn (Celem.term2str Celem.e_term (*t ..(t) has not been declared*))))
1.129 | parsitm dI (itm as (i, v, _, f, Model.Mis (d, t'))) =
1.130 (let val t = d $ t';
1.131 - val _ = term_to_string''' dI t;
1.132 + val _ = Celem.term_to_string''' dI t;
1.133 (*this ^ should raise the exn on unability of re-parsing dts*)
1.134 in itm end
1.135 - handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*))))
1.136 + handle _ => (i, v, false, f, Model.Syn (Celem.term2str Celem.e_term (*t ..(t) has not been declared*))))
1.137 | parsitm dI (itm as (_, _, _, _, Model.Par _)) =
1.138 - error ("parsitm (" ^ Model.itm2str_ (thy2ctxt dI) itm ^ "): Par should be internal");
1.139 + error ("parsitm (" ^ Model.itm2str_ (Celem.thy2ctxt dI) itm ^ "): Par should be internal");
1.140
1.141 (*separate a list to a pair of elements that do NOT satisfy the predicate,
1.142 and of elements that satisfy the predicate, i.e. (false, true)*)
1.143 @@ -181,7 +181,7 @@
1.144 (* WN.9.11.03 copied from fun appl_add *)
1.145 fun appl_add' dI oris ppc pbt (sel, ct) =
1.146 let
1.147 - val ctxt = assoc_thy dI |> thy2ctxt;
1.148 + val ctxt = Celem.assoc_thy dI |> Celem.thy2ctxt;
1.149 in
1.150 case TermC.parseNEW ctxt ct of
1.151 NONE => (0, [], false, sel, Model.Syn ct)
1.152 @@ -193,7 +193,7 @@
1.153 | (msg,_) => error ("appl_add': " ^ msg))
1.154 | (_, (i, v, _, d, ts), _) =>
1.155 if is_e_ts ts
1.156 - then (i, v, false, sel, Model.Inc ((d, ts), (e_term, [])))
1.157 + then (i, v, false, sel, Model.Inc ((d, ts), (Celem.e_term, [])))
1.158 else (i, v, false, sel, Model.Sup (d, ts)))
1.159 end
1.160
1.161 @@ -219,7 +219,7 @@
1.162 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
1.163 fun unknown_expl dI pbt selcts =
1.164 let
1.165 - val thy = assoc_thy dI
1.166 + val thy = Celem.assoc_thy dI
1.167 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
1.168 val its = Specify.add_id its_
1.169 in map flattup2 its end
1.170 @@ -239,19 +239,19 @@
1.171 fun oris2itms _ _ [] = [] (* WN161130: similar in ptyps ?!? *)
1.172 | oris2itms pbt vat ((i, v, f, d, ts) :: os) =
1.173 if member op = vat v
1.174 - then (i, v, true, f, Model.Cor ((d, ts), (e_term, []))) :: (oris2itms pbt vat os)
1.175 + then (i, v, true, f, Model.Cor ((d, ts), (Celem.e_term, []))) :: (oris2itms pbt vat os)
1.176 else oris2itms pbt vat os
1.177
1.178 fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
1.179 - | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (thy2ctxt' "Isac") itm)
1.180 + | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (Celem.thy2ctxt' "Isac") itm)
1.181 fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))
1.182 | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
1.183 | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
1.184 | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, Model.comp_dts'' (d,ts))
1.185 | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))
1.186 - | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, term2str (d $ t))
1.187 + | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, Celem.term2str (d $ t))
1.188 | itms2fstr (itm as (_, _, _, _, Model.Par _)) =
1.189 - error ("parsitm (" ^ Model.itm2str_ (thy2ctxt' "Isac") itm ^ "): Par should be internal");
1.190 + error ("parsitm (" ^ Model.itm2str_ (Celem.thy2ctxt' "Isac") itm ^ "): Par should be internal");
1.191
1.192 fun imodel2fstr iitems =
1.193 let
1.194 @@ -273,7 +273,7 @@
1.195 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
1.196 let val (pos_, pits, mits) =
1.197 if dI <> sdI
1.198 - then let val its = map (parsitm (assoc_thy dI)) probl;
1.199 + then let val its = map (parsitm (Celem.assoc_thy dI)) probl;
1.200 val (its, trms) = filter_sep is_Par its;
1.201 val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))
1.202 in (Ctree.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
1.203 @@ -284,7 +284,7 @@
1.204 let val pbt = (#ppc o Specify.get_pbt) pI
1.205 val dI' = #1 (Chead.some_spec ospec spec)
1.206 val oris = if pI = #2 ospec then oris
1.207 - else Specify.prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
1.208 + else Specify.prep_ori fmz_(Celem.assoc_thy"Isac") pbt |> #1;
1.209 in (Ctree.Pbl, appl_adds dI' oris probl pbt
1.210 (map itms2fstr probl), meth) end
1.211 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.212 @@ -299,12 +299,12 @@
1.213 val pt = Ctree.update_spec pt p spec;
1.214 in if pos_ = Ctree.Pbl
1.215 then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
1.216 - val pre = Stool.check_preconds (assoc_thy"Isac") prls where_ pits
1.217 + val pre = Stool.check_preconds (Celem.assoc_thy"Isac") prls where_ pits
1.218 in (Ctree.update_pbl pt p pits,
1.219 (Chead.ocalhd_complete pits pre spec, Ctree.Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
1.220 end
1.221 else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
1.222 - val pre = Stool.check_preconds (assoc_thy"Isac") prls pre mits
1.223 + val pre = Stool.check_preconds (Celem.assoc_thy"Isac") prls pre mits
1.224 in (Ctree.update_met pt p mits,
1.225 (Chead.ocalhd_complete mits pre spec, Ctree.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
1.226 end
1.227 @@ -336,20 +336,20 @@
1.228 (* 040214: version for concat_deriv *)
1.229 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
1.230
1.231 -fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) =
1.232 +fun mk_tacis ro erls (t, r as Celem.Thm (id, thm), (t', a)) =
1.233 (Tac.Rewrite (id, thm),
1.234 Tac.Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
1.235 (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Selem.Uistate, Selem.e_ctxt)))
1.236 - | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) =
1.237 + | mk_tacis _ _ (t, r as Celem.Rls_ rls, (t', a)) =
1.238 (Tac.Rewrite_Set (Lucin.rule2rls' r),
1.239 Tac.Rewrite_Set' ("Isac", false, rls, t, (t', a)),
1.240 (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Selem.Uistate, Selem.e_ctxt)))
1.241 - | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t)
1.242 + | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Celem.rule2str r ^ " at " ^ Celem.term2str t)
1.243
1.244 (* fo = ifo excluded already in inform *)
1.245 fun concat_deriv rew_ord erls rules fo ifo =
1.246 let
1.247 - fun derivat ([]:(term * rule * (term * term list)) list) = e_term
1.248 + fun derivat ([]:(term * Celem.rule * (term * term list)) list) = Celem.e_term
1.249 | derivat dt = (#1 o #3 o last_elem) dt
1.250 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
1.251 val fod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE fo
1.252 @@ -380,9 +380,9 @@
1.253 case p_ of
1.254 Ctree.Frm => Ctree.get_obj Ctree.g_form pt p
1.255 | Ctree.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.256 - | _ => e_term (*on PblObj is fo <> ifo*);
1.257 + | _ => Celem.e_term (*on PblObj is fo <> ifo*);
1.258 val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
1.259 - val {rew_ord, erls, rules, ...} = rep_rls nrls
1.260 + val {rew_ord, erls, rules, ...} = Celem.rep_rls nrls
1.261 val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
1.262 in
1.263 if found
1.264 @@ -410,10 +410,10 @@
1.265 end
1.266
1.267 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
1.268 -fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls =
1.269 +fun check_err_patt (res, inf) subst (errpatID, pat) rls =
1.270 let
1.271 val (res', _, _, rewritten) =
1.272 - Rewrite.rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) res;
1.273 + Rewrite.rew_sub (Isac()) 1 subst Celem.e_rew_ord Celem.e_rls false [] (HOLogic.Trueprop $ pat) res;
1.274 in
1.275 if rewritten
1.276 then
1.277 @@ -436,7 +436,7 @@
1.278 val (_, subst) = Rtools.get_bdv_subst prog env
1.279 fun scan (_, [], _) = NONE
1.280 | scan (errpatID, errpat :: errpats, _) =
1.281 - case check_err_patt (res, inf) (subst: subst) (errpatID, errpat) rls of
1.282 + case check_err_patt (res, inf) subst (errpatID, errpat) rls of
1.283 NONE => scan (errpatID, errpats, [])
1.284 | SOME errpatID => SOME errpatID
1.285 fun scans [] = NONE
1.286 @@ -456,7 +456,7 @@
1.287 if "no derivation found" then check_error_patterns.
1.288 ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
1.289 fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
1.290 - case TermC.parse (assoc_thy "Isac") istr of
1.291 + case TermC.parse (Celem.assoc_thy "Isac") istr of
1.292 SOME f_in =>
1.293 let
1.294 val f_in = Thm.term_of f_in
1.295 @@ -479,7 +479,7 @@
1.296 let
1.297 val pp = Ctree.par_pblobj pt p
1.298 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
1.299 - {errpats, nrls, scr = Prog prog, ...} => (errpats, nrls, prog)
1.300 + {errpats, nrls, scr = Celem.Prog prog, ...} => (errpats, nrls, prog)
1.301 | _ => error "inform: uncovered case of get_met"
1.302 val env = case Ctree.get_istate pt pos of
1.303 Selem.ScrState (env, _, _, _, _, _) => env
1.304 @@ -496,10 +496,10 @@
1.305
1.306 (* fill-in patterns an forms.
1.307 returns thm required by "fun in_fillform *)
1.308 -fun get_fillform (subs_opt, subst) (thm, form) errpatID ((fillpatID, pat, erpaID): fillpat) =
1.309 +fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
1.310 let
1.311 val (form', _, _, rewritten) =
1.312 - Rewrite.rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) form;
1.313 + Rewrite.rew_sub (Isac()) 1 subst Celem.e_rew_ord Celem.e_rls false [] (HOLogic.Trueprop $ pat) form;
1.314 in (*the fillpat of the thm must be dedicated to errpatID*)
1.315 if errpatID = erpaID andalso rewritten
1.316 then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
1.317 @@ -510,9 +510,9 @@
1.318 let
1.319 val thmDeriv = Thm.get_name_hint thm
1.320 val (part, thyID) = Rtools.thy_containing_thm thmDeriv
1.321 - val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
1.322 + val theID = [part, thyID, "Theorems", Celem.thmID_of_derivation_name thmDeriv]
1.323 val fillpats = case Specify.get_the theID of
1.324 - Hthm {fillpats, ...} => fillpats
1.325 + Celem.Hthm {fillpats, ...} => fillpats
1.326 | _ => error "get_fillpats: uncovered case of get_the"
1.327 val some = map (get_fillform subst (thm, form) errpatID) fillpats
1.328 in some |> filter is_some |> map the end
1.329 @@ -522,22 +522,22 @@
1.330 val f_curr = Ctree.get_curr_formula (pt, pos);
1.331 val pp = Ctree.par_pblobj pt p
1.332 val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
1.333 - {errpats, scr = Prog prog, ...} => (errpats, prog)
1.334 + {errpats, scr = Celem.Prog prog, ...} => (errpats, prog)
1.335 | _ => error "find_fillpatterns: uncovered case of get_met"
1.336 val env = case Ctree.get_istate pt pos of
1.337 Selem.ScrState (env, _, _, _, _, _) => env
1.338 | _ => error "inform: uncovered case of get_istate"
1.339 val subst = Rtools.get_bdv_subst prog env
1.340 val errpatthms = errpats
1.341 - |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
1.342 - |> map (#3: errpat -> thm list)
1.343 + |> filter ((curry op = errpatID) o (#1: Celem.errpat -> Celem.errpatID))
1.344 + |> map (#3: Celem.errpat -> thm list)
1.345 |> flat
1.346 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
1.347
1.348 (* check if an input formula is exactly equal the rewrite from a rule
1.349 which is stored at the pos where the input is stored of "ok". *)
1.350 fun is_exactly_equal (pt, pos as (p, _)) istr =
1.351 - case TermC.parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of
1.352 + case TermC.parseNEW (Celem.assoc_thy "Isac" |> Celem.thy2ctxt) istr of
1.353 NONE => ("syntax error in '" ^ istr ^ "'", Tac.Tac "")
1.354 | SOME ifo =>
1.355 let
1.356 @@ -569,13 +569,13 @@
1.357 | _ => "e_rls"
1.358 val (part, thyID) = Rtools.thy_containing_rls "Isac" rlsID;
1.359 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
1.360 - Hrls {thy_rls = (_, rls), ...} => rls
1.361 + Celem.Hrls {thy_rls = (_, rls), ...} => rls
1.362 | _ => error "fetchErrorpatterns: uncovered case of get_the"
1.363 in case rls of
1.364 - Rls {errpatts, ...} => errpatts
1.365 - | Seq {errpatts, ...} => errpatts
1.366 - | Rrls {errpatts, ...} => errpatts
1.367 - | Erls => []
1.368 + Celem.Rls {errpatts, ...} => errpatts
1.369 + | Celem.Seq {errpatts, ...} => errpatts
1.370 + | Celem.Rrls {errpatts, ...} => errpatts
1.371 + | Celem.Erls => []
1.372 end
1.373
1.374 (**)