1.1 --- a/src/Tools/isac/Specify/calchead.sml Wed Apr 15 16:46:41 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/calchead.sml Wed Apr 15 18:00:58 2020 +0200
1.3 @@ -364,9 +364,9 @@
1.4 else
1.5 case find_first (is_error o #5) pbl of
1.6 SOME (_, _, _, fd, itm_) =>
1.7 - (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
1.8 + (Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
1.9 | NONE =>
1.10 - (case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
1.11 + (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
1.12 SOME (fd, ct') => (Pbl, mk_additem fd ct')
1.13 | NONE => (*pbl-items complete*)
1.14 if not preok then (Pbl, Tactic.Refine_Problem pI')
1.15 @@ -375,16 +375,16 @@
1.16 else if mI = Celem.e_metID then (Pbl, Tactic.Specify_Method mI')
1.17 else
1.18 case find_first (is_error o #5) met of
1.19 - SOME (_, _, _, fd, itm_) => (Met, mk_delete (Celem.assoc_thy dI) fd itm_)
1.20 + SOME (_, _, _, fd, itm_) => (Met, mk_delete (ThyC.get_theory dI) fd itm_)
1.21 | NONE =>
1.22 - (case nxt_add (Celem.assoc_thy dI) oris mpc met of
1.23 + (case nxt_add (ThyC.get_theory dI) oris mpc met of
1.24 SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)
1.25 | NONE => (Met, Tactic.Apply_Method mI))))
1.26 | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
1.27 (case find_first (is_error o #5) met of
1.28 - SOME (_,_,_,fd,itm_) => (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
1.29 + SOME (_,_,_,fd,itm_) => (Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
1.30 | NONE =>
1.31 - case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
1.32 + case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
1.33 SOME (fd,ct') => (Met, mk_additem fd ct')
1.34 | NONE =>
1.35 (if dI = ThyC.id_empty then (Met, Tactic.Specify_Theory dI')
1.36 @@ -685,7 +685,7 @@
1.37 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
1.38 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
1.39 | _ => error "specify_additem: uncovered case of get_obj I pt p"
1.40 - val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI
1.41 + val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
1.42 val cpI = if pI = Celem.e_pblID then pI' else pI
1.43 val cmI = if mI = Celem.e_metID then mI' else mI
1.44 val {ppc, pre, prls, ...} = Specify.get_met cmI
1.45 @@ -727,7 +727,7 @@
1.46 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
1.47 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
1.48 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
1.49 - val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI
1.50 + val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
1.51 val cpI = if pI = Celem.e_pblID then pI' else pI
1.52 val cmI = if mI = Celem.e_metID then mI' else mI
1.53 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
1.54 @@ -773,7 +773,7 @@
1.55 PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
1.56 (oris, dI', pI', dI, pI, pbl, ctxt)
1.57 | _ => error "specify (Specify_Theory': uncovered case get_obj"
1.58 - val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI;
1.59 + val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
1.60 val cpI = if pI = Celem.e_pblID then pI' else pI;
1.61 in
1.62 case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
1.63 @@ -803,7 +803,7 @@
1.64 PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
1.65 (oris, dI', mI', dI, mI, met, ctxt)
1.66 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
1.67 - val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI;
1.68 + val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
1.69 val cmI = if mI = Celem.e_metID then mI' else mI;
1.70 in
1.71 case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
1.72 @@ -1173,7 +1173,7 @@
1.73 PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
1.74 | _ => error "get_ocalhd Pbl: uncovered case get_obj"
1.75 val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
1.76 - val pre = Stool.check_preconds (Celem.assoc_thy "Isac_Knowledge") prls where_ probl
1.77 + val pre = Stool.check_preconds (ThyC.get_theory "Isac_Knowledge") prls where_ probl
1.78 in
1.79 (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
1.80 end
1.81 @@ -1183,7 +1183,7 @@
1.82 PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
1.83 | _ => error "get_ocalhd Met: uncovered case get_obj"
1.84 val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
1.85 - val pre = Stool.check_preconds (Celem.assoc_thy "Isac_Knowledge") prls pre meth
1.86 + val pre = Stool.check_preconds (ThyC.get_theory "Isac_Knowledge") prls pre meth
1.87 in
1.88 (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
1.89 end