1.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Wed Apr 15 16:46:41 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Wed Apr 15 18:00:58 2020 +0200
1.3 @@ -52,7 +52,6 @@
1.4 val trace_calc: bool Unsynchronized.ref
1.5 val trace_rewrite: bool Unsynchronized.ref
1.6 val depth: int Unsynchronized.ref
1.7 - val assoc_thy: ThyC.id -> theory
1.8 val metID2str: string list -> string
1.9 val e_pblID: pblID
1.10 val e_metID: metID
1.11 @@ -324,11 +323,6 @@
1.12 type filepath = string;
1.13 type filename = string;
1.14
1.15 -fun assoc_thy thy =
1.16 - if thy = "thy_empty_id"
1.17 - then (ThyC.get_theory "Base_Tools") (*lower bound of Knowledge*)
1.18 - else (ThyC.get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
1.19 -
1.20 (* overwrite an element in an association list and pair it with a thyID
1.21 in order to create the thy_hierarchy;
1.22 overwrites existing rls' even if they are defined in a different thy;
2.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Wed Apr 15 16:46:41 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Wed Apr 15 18:00:58 2020 +0200
2.3 @@ -18,7 +18,7 @@
2.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.5 (*NONE*)
2.6 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.7 - (*NONE*)
2.8 + val get_thy: id -> theory
2.9 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.10 end
2.11
2.12 @@ -30,7 +30,13 @@
2.13 type id = string;
2.14 fun cut_id dn = hd (space_explode "." dn);
2.15
2.16 -fun get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID);
2.17 +
2.18 +fun get_thy thyID = Thy_Info.get_theory ("Isac." ^ thyID);
2.19 +fun get_theory thy =
2.20 + if thy = "thy_empty_id"
2.21 + then (get_thy "Base_Tools") (*lower bound of Knowledge*)
2.22 + else (get_thy thy) handle _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
2.23 +
2.24 fun id_to_ctxt thy' = Proof_Context.init_global (get_theory thy');
2.25 fun to_ctxt thy = Proof_Context.init_global thy;
2.26
3.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Wed Apr 15 16:46:41 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Wed Apr 15 18:00:58 2020 +0200
3.3 @@ -14,6 +14,7 @@
3.4 ML_file interface.sml
3.5
3.6 ML \<open>
3.7 +open ThyC
3.8 \<close> ML \<open>
3.9 \<close> ML \<open>
3.10 \<close>
4.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 15 16:46:41 2020 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 15 18:00:58 2020 +0200
4.3 @@ -452,13 +452,13 @@
4.4 XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
4.5 | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
4.6 fun xml_of_subs (subs : Selem.subs) =
4.7 - XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.subs2subst (Celem.assoc_thy "Isac_Knowledge") subs))
4.8 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.subs2subst (ThyC.get_theory "Isac_Knowledge") subs))
4.9 fun xml_to_subs
4.10 (XML.Elem (("SUBSTITUTION", []),
4.11 subs)) = Selem.subst2subs (map xml_to_sub subs)
4.12 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
4.13 fun xml_of_sube sube =
4.14 - XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.sube2subst (Celem.assoc_thy "Isac_Knowledge") sube))
4.15 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.sube2subst (ThyC.get_theory "Isac_Knowledge") sube))
4.16 fun xml_to_sube
4.17 (XML.Elem (("SUBSTITUTION", []),
4.18 xml_var_val_pairs)) = Selem.subst2sube (map xml_to_sub xml_var_val_pairs)
5.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 15 16:46:41 2020 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 15 18:00:58 2020 +0200
5.3 @@ -111,7 +111,7 @@
5.4 let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)
5.5 in map (makeHcal (part, thy')) cals end;
5.6 fun collect_ords (part, thy') =
5.7 - let val thy = Celem.assoc_thy thy'
5.8 + let val thy = ThyC.get_theory thy'
5.9 in [(*TODO.WN060120 rew_ord, Eval*)]:(Celem.theID * Celem.thydata) list end;
5.10
5.11 (* parts are: Isabelle | IsacKnowledge | IsacScripts, see KEStore.thy *)
6.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 16:46:41 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 18:00:58 2020 +0200
6.3 @@ -178,7 +178,7 @@
6.4 (* check if an input formula is exactly equal the rewrite from a rule
6.5 which is stored at the pos where the input is stored of "ok". *)
6.6 fun is_exactly_equal (pt, pos as (p, _)) istr =
6.7 - case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> ThyC.to_ctxt) istr of
6.8 + case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) istr of
6.9 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
6.10 | SOME ifo =>
6.11 let
7.1 --- a/src/Tools/isac/Interpret/li-tool.sml Wed Apr 15 16:46:41 2020 +0200
7.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 15 18:00:58 2020 +0200
7.3 @@ -177,12 +177,12 @@
7.4 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
7.5 else Not_Associated
7.6 | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
7.7 - if Rtools.contains_rule (Rule.Eval (assoc_calc' (Celem.assoc_thy "Isac_Knowledge")
7.8 + if Rtools.contains_rule (Rule.Eval (assoc_calc' (ThyC.get_theory "Isac_Knowledge")
7.9 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
7.10 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
7.11 else Not_Associated
7.12 | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
7.13 - if Rtools.contains_rule (Rule.Eval (assoc_calc' ( Celem.assoc_thy "Isac_Knowledge")
7.14 + if Rtools.contains_rule (Rule.Eval (assoc_calc' ( ThyC.get_theory "Isac_Knowledge")
7.15 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
7.16 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
7.17 else Not_Associated
7.18 @@ -325,7 +325,7 @@
7.19 end
7.20 else
7.21 (get_loc pt (p, p_),
7.22 - Rule.Prog (Auto_Prog.gen (Celem.assoc_thy thy) (get_last_formula (pt, (p, p_))) rls'))
7.23 + Rule.Prog (Auto_Prog.gen (ThyC.get_theory thy) (get_last_formula (pt, (p, p_))) rls'))
7.24 end
7.25
7.26
8.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 15 16:46:41 2020 +0200
8.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 15 18:00:58 2020 +0200
8.3 @@ -322,7 +322,7 @@
8.4 (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
8.5 AssOnly => Term_Val1 act_arg
8.6 | _(*ORundef*) =>
8.7 - case Applicable.applicable_in p pt (LItool.tac_from_prog pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of
8.8 + case Applicable.applicable_in p pt (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) of
8.9 Applicable.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
8.10 | Applicable.Notappl _ => Term_Val1 act_arg)
8.11
9.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 15 16:46:41 2020 +0200
9.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 15 18:00:58 2020 +0200
9.3 @@ -343,7 +343,7 @@
9.4 val thm_deriv = Thm.get_name_hint thm
9.5 val pp = Ctree.par_pblobj pt p
9.6 val thy' = Ctree.get_obj Ctree.g_domID pt pp
9.7 - val subst = Selem.subs2subst (Celem.assoc_thy thy') subs
9.8 + val subst = Selem.subs2subst (ThyC.get_theory thy') subs
9.9 val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
9.10 val f = case p_ of
9.11 Pos.Frm => Ctree.get_obj Ctree.g_form pt p
9.12 @@ -494,7 +494,7 @@
9.13 [isa, thy, sect, xstr] => (isa, thy, sect, xstr)
9.14 | _ => error "guh2rewtac: uncovered case"
9.15 in case sect of
9.16 - "Theorems" => Tactic.Rewrite (xstr, ThmC.thm_from_thy (Celem.assoc_thy thy) xstr)
9.17 + "Theorems" => Tactic.Rewrite (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr)
9.18 | "Rulesets" => Tactic.Rewrite_Set xstr
9.19 | _ => error ("guh2rewtac: not impl. for '"^xstr^"'")
9.20 end
9.21 @@ -505,7 +505,7 @@
9.22 | _ => error "guh2rewtac: uncovered case"
9.23 in case sect of
9.24 "Theorems" =>
9.25 - Tactic.Rewrite_Inst (subs, (xstr, ThmC.thm_from_thy (Celem.assoc_thy thy) xstr))
9.26 + Tactic.Rewrite_Inst (subs, (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr))
9.27 | "Rulesets" => Tactic.Rewrite_Set_Inst (subs, xstr)
9.28 | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
9.29 end
9.30 @@ -529,7 +529,7 @@
9.31 in
9.32 case sect of
9.33 "Theorems" =>
9.34 - let val thm = Global_Theory.get_thm (Celem.assoc_thy thyID) xstr
9.35 + let val thm = Global_Theory.get_thm (ThyC.get_theory thyID) xstr
9.36 in
9.37 if Auto_Prog.contains_bdv thm
9.38 then
10.1 --- a/src/Tools/isac/Interpret/step-solve.sml Wed Apr 15 16:46:41 2020 +0200
10.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Wed Apr 15 18:00:58 2020 +0200
10.3 @@ -74,7 +74,7 @@
10.4 end
10.5 | _ => (* NotLocatable *)
10.6 let
10.7 - val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, p_) pt;
10.8 + val (p,ps, _, pt) = Generate.generate_hard (ThyC.get_theory "Isac_Knowledge") m (p, p_) pt;
10.9 in
10.10 ("not-found-in-program", ([(Tactic.input_from_T m, m, (po, is))], ps, (pt, p)))
10.11 end
10.12 @@ -91,7 +91,7 @@
10.13 *)
10.14 (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =*)
10.15 fun by_term (pt, pos as (p, _)) istr =
10.16 - case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of
10.17 + case TermC.parse (ThyC.get_theory "Isac_Knowledge") istr of
10.18 NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')
10.19 | SOME f_in =>
10.20 let
11.1 --- a/src/Tools/isac/Interpret/sub-problem.sml Wed Apr 15 16:46:41 2020 +0200
11.2 +++ b/src/Tools/isac/Interpret/sub-problem.sml Wed Apr 15 18:00:58 2020 +0200
11.3 @@ -17,7 +17,7 @@
11.4 fun tac_from_prog pt (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags') =
11.5 let
11.6 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
11.7 - val thy = Stool.common_subthy (Celem.assoc_thy dI, Ctree.rootthy pt);
11.8 + val thy = Stool.common_subthy (ThyC.get_theory dI, Ctree.rootthy pt);
11.9 val ags = TermC.isalist2list ags';
11.10 val (pI, pors, mI) =
11.11 if mI = ["no_met"]
11.12 @@ -37,7 +37,7 @@
11.13 val (fmz_, vals) = Chead.oris2fmz_vals pors;
11.14 val {cas, ppc, thy, ...} = Specify.get_pbt pI
11.15 val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
11.16 - val dI = Context.theory_name (Stool.common_subthy (Celem.assoc_thy dI, Ctree.rootthy pt))
11.17 + val dI = Context.theory_name (Stool.common_subthy (ThyC.get_theory dI, Ctree.rootthy pt))
11.18 val ctxt = ContextC.initialise dI vals
11.19 val hdl =
11.20 case cas of
12.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 15 16:46:41 2020 +0200
12.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 15 18:00:58 2020 +0200
12.3 @@ -147,7 +147,7 @@
12.4 | ord => ord)
12.5 and hd_ord (f, g) = (* ~ term.ML *)
12.6 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
12.7 -and terms_ord str pr (ts, us) = list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
12.8 +and terms_ord str pr (ts, us) = list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
12.9 (**)
12.10 in
12.11 (**)
13.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Apr 15 16:46:41 2020 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Apr 15 18:00:58 2020 +0200
13.3 @@ -501,7 +501,7 @@
13.4 and hd_ord (f, g) = (* ~ term.ML *)
13.5 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
13.6 and terms_ord _ pr (ts, us) =
13.7 - list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
13.8 + list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
13.9
13.10 in
13.11
14.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Apr 15 16:46:41 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Apr 15 18:00:58 2020 +0200
14.3 @@ -1214,7 +1214,7 @@
14.4 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)
14.5 int_ord (dest_hd' x f, dest_hd' x g)
14.6 and terms_ord x str pr (ts, us) =
14.7 - list_ord (term_ord' x pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
14.8 + list_ord (term_ord' x pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
14.9
14.10 in
14.11
15.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Apr 15 16:46:41 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Apr 15 18:00:58 2020 +0200
15.3 @@ -137,7 +137,7 @@
15.4 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
15.5 (dest_hd' f, dest_hd' g)
15.6 and terms_ord str pr (ts, us) =
15.7 - list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
15.8 + list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
15.9
15.10 in
15.11 (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
16.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Apr 15 16:46:41 2020 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Apr 15 18:00:58 2020 +0200
16.3 @@ -342,7 +342,7 @@
16.4 and hd_ord (f, g) = (* ~ term.ML *)
16.5 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
16.6 and terms_ord str pr (ts, us) =
16.7 - list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
16.8 + list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
16.9 in
16.10
16.11 fun ord_make_polytest (pr:bool) thy (_: UnparseC.subst) tu =
17.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 15 16:46:41 2020 +0200
17.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 15 18:00:58 2020 +0200
17.3 @@ -820,7 +820,7 @@
17.4
17.5 (* get the theory explicitly specified for the rootpbl;
17.6 thus use this function _after_ finishing specification *)
17.7 -fun rootthy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Celem.assoc_thy thyID
17.8 +fun rootthy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = ThyC.get_theory thyID
17.9 | rootthy _ = error "rootthy: uncovered fun def.";
17.10
17.11 (**)
18.1 --- a/src/Tools/isac/MathEngBasic/mstools.sml Wed Apr 15 16:46:41 2020 +0200
18.2 +++ b/src/Tools/isac/MathEngBasic/mstools.sml Wed Apr 15 18:00:58 2020 +0200
18.3 @@ -72,7 +72,7 @@
18.4 (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
18.5 (false, pre)
18.6 | evalprecond prls (true, pre) =
18.7 - if Rewrite.eval_true (Celem.assoc_thy "Isac_Knowledge") (* for Pattern.match *)
18.8 + if Rewrite.eval_true (ThyC.get_theory "Isac_Knowledge") (* for Pattern.match *)
18.9 [pre] prls (* pre parsed, prls.thy *)
18.10 then (true , pre)
18.11 else (false , pre);
18.12 @@ -93,6 +93,6 @@
18.13 fun common_subthy (thy1, thy2) =
18.14 if Context.subthy (thy1, thy2) then thy2
18.15 else if Context.subthy (thy2, thy1) then thy1
18.16 - else Celem.assoc_thy "Isac_Knowledge"
18.17 + else ThyC.get_theory "Isac_Knowledge"
18.18
18.19 end;
19.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Wed Apr 15 16:46:41 2020 +0200
19.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Wed Apr 15 18:00:58 2020 +0200
19.3 @@ -28,7 +28,7 @@
19.4 let
19.5 val pp = par_pblobj pt p;
19.6 val thy' = get_obj g_domID pt pp;
19.7 - val thy = Celem.assoc_thy thy';
19.8 + val thy = ThyC.get_theory thy';
19.9 val metID = get_obj g_metID pt pp;
19.10 val metID' = if metID = Celem.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
19.11 val (sc, srls) = (case Specify.get_met metID' of
19.12 @@ -50,7 +50,7 @@
19.13 let
19.14 val pp = par_pblobj pt p
19.15 val thy' = get_obj g_domID pt pp
19.16 - val thy = Celem.assoc_thy thy'
19.17 + val thy = ThyC.get_theory thy'
19.18 val metID = get_obj g_metID pt pp
19.19 val metID' =
19.20 if metID = Celem.e_metID
20.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 15 16:46:41 2020 +0200
20.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 15 18:00:58 2020 +0200
20.3 @@ -148,7 +148,7 @@
20.4 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
20.5 else pI'
20.6 val {ppc, where_, prls, ...} = Specify.get_pbt pblID
20.7 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") probl (ppc, where_, prls) os
20.8 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
20.9 in
20.10 (model_ok, pblID, hdl, pbl, pre)
20.11 end
20.12 @@ -163,7 +163,7 @@
20.13 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
20.14 else mI'
20.15 val {ppc, pre, prls, scr, ...} = Specify.get_met metID
20.16 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") meth (ppc,pre,prls) os
20.17 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
20.18 in
20.19 (model_ok, metID, scr, pbl, pre)
20.20 end
20.21 @@ -176,7 +176,7 @@
20.22 Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
20.23 | Ctree.PrfObj _ => error "context_pbl: uncovered case"
20.24 val {ppc,where_,prls,...} = Specify.get_pbt pI
20.25 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") probl (ppc,where_,prls) os
20.26 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
20.27 in
20.28 (model_ok, pI, hdl, pbl, pre)
20.29 end
20.30 @@ -188,7 +188,7 @@
20.31 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
20.32 | Ctree.PrfObj _ => error "context_met: uncovered case"
20.33 val {ppc,pre,prls,scr,...} = Specify.get_met mI
20.34 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") meth (ppc,pre,prls) os
20.35 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
20.36 in
20.37 (model_ok, mI, scr, pbl, pre)
20.38 end
20.39 @@ -200,11 +200,11 @@
20.40 Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
20.41 | Ctree.PrfObj _ => error "context_met: uncovered case"
20.42 in
20.43 - case Specify.refine_pbl (Celem.assoc_thy "Isac_Knowledge") pI probl of
20.44 + case Specify.refine_pbl (ThyC.get_theory "Isac_Knowledge") pI probl of
20.45 NONE => (*copy from context_pbl*)
20.46 let
20.47 val {ppc,where_,prls,...} = Specify.get_pbt pI
20.48 - val (_, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") probl (ppc,where_,prls) os
20.49 + val (_, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
20.50 in
20.51 (false, pI, hdl, pbl, pre)
20.52 end
21.1 --- a/src/Tools/isac/Specify/appl.sml Wed Apr 15 16:46:41 2020 +0200
21.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Apr 15 18:00:58 2020 +0200
21.3 @@ -162,7 +162,7 @@
21.4 | _ => error "applicable_in Refine_Problem: uncovered case get_obj"
21.5 val thy = if dI' = ThyC.id_empty then dI else dI';
21.6 in
21.7 - case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of
21.8 + case Specify.refine_pbl (ThyC.get_theory thy) pI itms of
21.9 NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
21.10 | SOME (rf as (pI', _)) =>
21.11 if pI' = pI
21.12 @@ -208,7 +208,7 @@
21.13 PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
21.14 => (oris, dI, pI, dI', pI', itms)
21.15 | _ => error "applicable_in Specify_Problem: uncovered case get_obj"
21.16 - val thy = Celem.assoc_thy (if dI' = ThyC.id_empty then dI else dI');
21.17 + val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
21.18 val {ppc, where_, prls, ...} = Specify.get_pbt pID;
21.19 val pbl = if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
21.20 then (false, (Generate.init_pbl ppc, []))
21.21 @@ -231,7 +231,7 @@
21.22 val {where_, ...} = Specify.get_pbt pI
21.23 val pres = map (Model.mk_env probl |> subst_atomic) where_
21.24 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
21.25 - then Celem.assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
21.26 + then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
21.27 else ctxt
21.28 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
21.29 and then decide on Notappl/Appl accordingly once more.
21.30 @@ -253,7 +253,7 @@
21.31 let
21.32 val pp = par_pblobj pt p;
21.33 val thy' = get_obj g_domID pt pp;
21.34 - val thy = Celem.assoc_thy thy';
21.35 + val thy = ThyC.get_theory thy';
21.36 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);
21.37 val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
21.38 Frm => (get_obj g_form pt p, p)
21.39 @@ -276,7 +276,7 @@
21.40 else
21.41 let
21.42 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;
21.43 - val thy = Celem.assoc_thy thy';
21.44 + val thy = ThyC.get_theory thy';
21.45 val f = case p_ of
21.46 Frm => get_obj g_form pt p
21.47 | Res => (fst o (get_obj g_result pt)) p
21.48 @@ -296,7 +296,7 @@
21.49 let
21.50 val pp = par_pblobj pt p;
21.51 val thy' = get_obj g_domID pt pp;
21.52 - val thy = Celem.assoc_thy thy';
21.53 + val thy = ThyC.get_theory thy';
21.54 val f = case p_ of Frm => get_obj g_form pt p
21.55 | Res => (fst o (get_obj g_result pt)) p
21.56 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
21.57 @@ -315,7 +315,7 @@
21.58 let
21.59 val pp = par_pblobj pt p;
21.60 val thy' = get_obj g_domID pt pp;
21.61 - val thy = Celem.assoc_thy thy';
21.62 + val thy = ThyC.get_theory thy';
21.63 val (f, _) = case p_ of
21.64 Frm => (get_obj g_form pt p, p)
21.65 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
21.66 @@ -340,7 +340,7 @@
21.67 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
21.68 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
21.69 in
21.70 - case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of
21.71 + case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
21.72 SOME (f', asm)
21.73 => Appl (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
21.74 | NONE => Notappl (rls ^ " not applicable")
21.75 @@ -357,7 +357,7 @@
21.76 | Res => (fst o (get_obj g_result pt)) p
21.77 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
21.78 in
21.79 - case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of
21.80 + case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
21.81 SOME (f',asm) => Appl (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
21.82 | NONE => Notappl (rls^" not applicable")
21.83 end
21.84 @@ -375,7 +375,7 @@
21.85 in
21.86 if msg = "OK"
21.87 then
21.88 - case Rewrite.calculate_ (Celem.assoc_thy thy') isa_fn f of
21.89 + case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
21.90 SOME (f', (id, thm))
21.91 => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
21.92 | NONE => Notappl ("'calculate "^op_^"' not applicable")
21.93 @@ -390,7 +390,7 @@
21.94 else
21.95 let
21.96 val pp = par_pblobj pt p
21.97 - val thy = Celem.assoc_thy (get_obj g_domID pt pp)
21.98 + val thy = ThyC.get_theory (get_obj g_domID pt pp)
21.99 val f = case p_ of
21.100 Frm => get_obj g_form pt p
21.101 | Res => (fst o (get_obj g_result pt)) p
21.102 @@ -464,7 +464,7 @@
21.103 let
21.104 val pp = par_pblobj pt p;
21.105 val thy' = get_obj g_domID pt pp;
21.106 - val thy = Celem.assoc_thy thy'
21.107 + val thy = ThyC.get_theory thy'
21.108 val metID = (get_obj g_metID pt pp)
21.109 val {crls, ...} = Specify.get_met metID
21.110 val (f, asm) = case p_ of
21.111 @@ -495,7 +495,7 @@
21.112 let
21.113 val pp = par_pblobj pt p;
21.114 val thy' = get_obj g_domID pt pp;
21.115 - val thy = Celem.assoc_thy thy';
21.116 + val thy = ThyC.get_theory thy';
21.117 val f = case p_ of
21.118 Frm => get_obj g_form pt p
21.119 | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"
22.1 --- a/src/Tools/isac/Specify/calchead.sml Wed Apr 15 16:46:41 2020 +0200
22.2 +++ b/src/Tools/isac/Specify/calchead.sml Wed Apr 15 18:00:58 2020 +0200
22.3 @@ -364,9 +364,9 @@
22.4 else
22.5 case find_first (is_error o #5) pbl of
22.6 SOME (_, _, _, fd, itm_) =>
22.7 - (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
22.8 + (Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
22.9 | NONE =>
22.10 - (case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
22.11 + (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
22.12 SOME (fd, ct') => (Pbl, mk_additem fd ct')
22.13 | NONE => (*pbl-items complete*)
22.14 if not preok then (Pbl, Tactic.Refine_Problem pI')
22.15 @@ -375,16 +375,16 @@
22.16 else if mI = Celem.e_metID then (Pbl, Tactic.Specify_Method mI')
22.17 else
22.18 case find_first (is_error o #5) met of
22.19 - SOME (_, _, _, fd, itm_) => (Met, mk_delete (Celem.assoc_thy dI) fd itm_)
22.20 + SOME (_, _, _, fd, itm_) => (Met, mk_delete (ThyC.get_theory dI) fd itm_)
22.21 | NONE =>
22.22 - (case nxt_add (Celem.assoc_thy dI) oris mpc met of
22.23 + (case nxt_add (ThyC.get_theory dI) oris mpc met of
22.24 SOME (fd, ct') => (Met, mk_additem fd ct') (*30.8.01: pre?!?*)
22.25 | NONE => (Met, Tactic.Apply_Method mI))))
22.26 | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
22.27 (case find_first (is_error o #5) met of
22.28 - SOME (_,_,_,fd,itm_) => (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
22.29 + SOME (_,_,_,fd,itm_) => (Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
22.30 | NONE =>
22.31 - case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
22.32 + case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
22.33 SOME (fd,ct') => (Met, mk_additem fd ct')
22.34 | NONE =>
22.35 (if dI = ThyC.id_empty then (Met, Tactic.Specify_Theory dI')
22.36 @@ -685,7 +685,7 @@
22.37 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
22.38 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
22.39 | _ => error "specify_additem: uncovered case of get_obj I pt p"
22.40 - val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI
22.41 + val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
22.42 val cpI = if pI = Celem.e_pblID then pI' else pI
22.43 val cmI = if mI = Celem.e_metID then mI' else mI
22.44 val {ppc, pre, prls, ...} = Specify.get_met cmI
22.45 @@ -727,7 +727,7 @@
22.46 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
22.47 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
22.48 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
22.49 - val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI
22.50 + val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
22.51 val cpI = if pI = Celem.e_pblID then pI' else pI
22.52 val cmI = if mI = Celem.e_metID then mI' else mI
22.53 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
22.54 @@ -773,7 +773,7 @@
22.55 PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
22.56 (oris, dI', pI', dI, pI, pbl, ctxt)
22.57 | _ => error "specify (Specify_Theory': uncovered case get_obj"
22.58 - val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI;
22.59 + val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
22.60 val cpI = if pI = Celem.e_pblID then pI' else pI;
22.61 in
22.62 case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
22.63 @@ -803,7 +803,7 @@
22.64 PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
22.65 (oris, dI', mI', dI, mI, met, ctxt)
22.66 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
22.67 - val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI;
22.68 + val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
22.69 val cmI = if mI = Celem.e_metID then mI' else mI;
22.70 in
22.71 case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
22.72 @@ -1173,7 +1173,7 @@
22.73 PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
22.74 | _ => error "get_ocalhd Pbl: uncovered case get_obj"
22.75 val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
22.76 - val pre = Stool.check_preconds (Celem.assoc_thy "Isac_Knowledge") prls where_ probl
22.77 + val pre = Stool.check_preconds (ThyC.get_theory "Isac_Knowledge") prls where_ probl
22.78 in
22.79 (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
22.80 end
22.81 @@ -1183,7 +1183,7 @@
22.82 PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
22.83 | _ => error "get_ocalhd Met: uncovered case get_obj"
22.84 val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
22.85 - val pre = Stool.check_preconds (Celem.assoc_thy "Isac_Knowledge") prls pre meth
22.86 + val pre = Stool.check_preconds (ThyC.get_theory "Isac_Knowledge") prls pre meth
22.87 in
22.88 (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
22.89 end
23.1 --- a/src/Tools/isac/Specify/generate.sml Wed Apr 15 16:46:41 2020 +0200
23.2 +++ b/src/Tools/isac/Specify/generate.sml Wed Apr 15 18:00:58 2020 +0200
23.3 @@ -46,14 +46,14 @@
23.4 (* initialize istate for Detail_Set *)
23.5 fun init_istate (Tactic.Rewrite_Set rls) t =
23.6 let
23.7 - val thy = Celem.assoc_thy "Isac_Knowledge"
23.8 + val thy = ThyC.get_theory "Isac_Knowledge"
23.9 val args = Auto_Prog.gen thy t (assoc_rls rls) |> Program.formal_args
23.10 in
23.11 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)])
23.12 end
23.13 | init_istate (Tactic.Rewrite_Set_Inst (subs, rls)) t =
23.14 let
23.15 - val thy = Celem.assoc_thy "Isac_Knowledge"
23.16 + val thy = ThyC.get_theory "Isac_Knowledge"
23.17 val rls' = assoc_rls rls
23.18 val v = case Selem.subs2subst thy subs of
23.19 (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)
24.1 --- a/src/Tools/isac/Specify/input-calchead.sml Wed Apr 15 16:46:41 2020 +0200
24.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Wed Apr 15 18:00:58 2020 +0200
24.3 @@ -40,7 +40,7 @@
24.4
24.5 fun cas_input_ ((dI, pI, mI): Celem.spec) dtss = (*WN110515 reconsider thy..ctxt*)
24.6 let
24.7 - val thy = Celem.assoc_thy dI
24.8 + val thy = ThyC.get_theory dI
24.9 val {ppc, ...} = Specify.get_pbt pI
24.10 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
24.11 val its = Specify.add_id its_
24.12 @@ -66,7 +66,7 @@
24.13 let
24.14 val (h, argl) = strip_comb hdt
24.15 in
24.16 - case assoc_cas (Celem.assoc_thy "Isac_Knowledge") h of
24.17 + case assoc_cas (ThyC.get_theory "Isac_Knowledge") h of
24.18 NONE => NONE
24.19 | SOME (spec as (dI,_,_), argl2dtss) =>
24.20 let
24.21 @@ -162,7 +162,7 @@
24.22 (* WN.9.11.03 copied from fun appl_add *)
24.23 fun appl_add' dI oris ppc pbt (sel, ct) =
24.24 let
24.25 - val ctxt = Celem.assoc_thy dI |> ThyC.to_ctxt;
24.26 + val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt;
24.27 in
24.28 case TermC.parseNEW ctxt ct of
24.29 NONE => (0, [], false, sel, Model.Syn ct)
24.30 @@ -200,7 +200,7 @@
24.31 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
24.32 fun unknown_expl dI pbt selcts =
24.33 let
24.34 - val thy = Celem.assoc_thy dI
24.35 + val thy = ThyC.get_theory dI
24.36 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
24.37 val its = Specify.add_id its_
24.38 in map flattup2 its end
24.39 @@ -254,7 +254,7 @@
24.40 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
24.41 let val (pos_, pits, mits) =
24.42 if dI <> sdI
24.43 - then let val its = map (parsitm (Celem.assoc_thy dI)) probl;
24.44 + then let val its = map (parsitm (ThyC.get_theory dI)) probl;
24.45 val (its, trms) = filter_sep is_Par its;
24.46 val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))
24.47 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
24.48 @@ -265,7 +265,7 @@
24.49 let val pbt = (#ppc o Specify.get_pbt) pI
24.50 val dI' = #1 (Chead.some_spec ospec spec)
24.51 val oris = if pI = #2 ospec then oris
24.52 - else Specify.prep_ori fmz_(Celem.assoc_thy"Isac_Knowledge") pbt |> #1;
24.53 + else Specify.prep_ori fmz_(ThyC.get_theory"Isac_Knowledge") pbt |> #1;
24.54 in (Pos.Pbl, appl_adds dI' oris probl pbt
24.55 (map itms2fstr probl), meth) end
24.56 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
24.57 @@ -280,12 +280,12 @@
24.58 val pt = Ctree.update_spec pt p spec;
24.59 in if pos_ = Pos.Pbl
24.60 then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
24.61 - val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls where_ pits
24.62 + val pre = Stool.check_preconds (ThyC.get_theory"Isac_Knowledge") prls where_ pits
24.63 in (Ctree.update_pbl pt p pits,
24.64 (Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
24.65 end
24.66 else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
24.67 - val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls pre mits
24.68 + val pre = Stool.check_preconds (ThyC.get_theory"Isac_Knowledge") prls pre mits
24.69 in (Ctree.update_met pt p mits,
24.70 (Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
24.71 end
25.1 --- a/src/Tools/isac/Specify/specify.sml Wed Apr 15 16:46:41 2020 +0200
25.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Apr 15 18:00:58 2020 +0200
25.3 @@ -48,9 +48,9 @@
25.4 else
25.5 case find_first (is_error o #5) pbl of
25.6 SOME (_, _, _, fd, itm_) =>
25.7 - ("dummy", (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
25.8 + ("dummy", (Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
25.9 | NONE =>
25.10 - (case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
25.11 + (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
25.12 SOME (fd, ct') => ("dummy", (Pbl, mk_additem fd ct'))
25.13 | NONE => (*pbl-items complete*)
25.14 if not preok then ("dummy", (Pbl, Tactic.Refine_Problem pI'))
25.15 @@ -59,16 +59,16 @@
25.16 else if mI = Celem.e_metID then ("dummy", (Pbl, Tactic.Specify_Method mI'))
25.17 else
25.18 case find_first (is_error o #5) met of
25.19 - SOME (_, _, _, fd, itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy dI) fd itm_))
25.20 + SOME (_, _, _, fd, itm_) => ("dummy", (Met, mk_delete (ThyC.get_theory dI) fd itm_))
25.21 | NONE =>
25.22 - (case nxt_add (Celem.assoc_thy dI) oris mpc met of
25.23 + (case nxt_add (ThyC.get_theory dI) oris mpc met of
25.24 SOME (fd, ct') => ("dummy", (Met, mk_additem fd ct')) (*30.8.01: pre?!?*)
25.25 | NONE => ("dummy", (Met, Tactic.Apply_Method mI)))))
25.26 | Met =>
25.27 (case find_first (is_error o #5) met of
25.28 - SOME (_,_,_,fd,itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
25.29 + SOME (_,_,_,fd,itm_) => ("dummy", (Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
25.30 | NONE =>
25.31 - case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
25.32 + case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
25.33 SOME (fd,ct') => ("dummy", (Met, mk_additem fd ct'))
25.34 | NONE =>
25.35 (if dI = ThyC.id_empty then ("dummy", (Met, Tactic.Specify_Theory dI'))
25.36 @@ -113,7 +113,7 @@
25.37 in ((pt, ([], Pbl)), []) end
25.38 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
25.39 let (* both """"""""""""""""""""""""" either empty or complete *)
25.40 - val thy = Celem.assoc_thy dI
25.41 + val thy = ThyC.get_theory dI
25.42 val (pI, (pors, pctxt), mI) =
25.43 if mI = ["no_met"]
25.44 then
26.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Apr 15 16:46:41 2020 +0200
26.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Apr 15 18:00:58 2020 +0200
26.3 @@ -31,7 +31,7 @@
26.4 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
26.5 | _ => error "by_tactic_input Model_Problem; uncovered case get_obj"
26.6 val (dI, pI, mI) = some_spec ospec spec
26.7 - val thy = Celem.assoc_thy dI
26.8 + val thy = ThyC.get_theory dI
26.9 val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
26.10 val {cas, ppc, ...} = Specify.get_pbt pI
26.11 val pbl = Generate.init_pbl ppc (* fill in descriptions *)
26.12 @@ -61,7 +61,7 @@
26.13 val {met, ...} = Specify.get_pbt pI'
26.14 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
26.15 val mI = if length met = 0 then Celem.e_metID else hd met
26.16 - val thy = Celem.assoc_thy dI
26.17 + val thy = ThyC.get_theory dI
26.18 val (pos, c, _, pt) =
26.19 Generate.generate1 (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
26.20 in
26.21 @@ -78,7 +78,7 @@
26.22 | _ => error "by_tactic_input Refine_Problem: uncovered case get_obj"
26.23 val thy = if dI' = ThyC.id_empty then dI else dI'
26.24 in
26.25 - case Specify.refine_pbl (Celem.assoc_thy thy) pI probl of
26.26 + case Specify.refine_pbl (ThyC.get_theory thy) pI probl of
26.27 NONE => ([], [], ptp)
26.28 | SOME rfd =>
26.29 let
26.30 @@ -93,7 +93,7 @@
26.31 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
26.32 (oris, dI, dI', pI', probl, ctxt)
26.33 | _ => error ""
26.34 - val thy = Celem.assoc_thy (if dI' = ThyC.id_empty then dI else dI');
26.35 + val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
26.36 val {ppc,where_,prls,...} = Specify.get_pbt pI
26.37 val pbl =
26.38 if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
26.39 @@ -116,7 +116,7 @@
26.40 => (oris, pbl, dI, met, ctxt)
26.41 | _ => error "by_tactic_input Specify_Method: uncovered case get_obj"
26.42 val {ppc,pre,prls,...} = Specify.get_met mID
26.43 - val thy = Celem.assoc_thy dI
26.44 + val thy = ThyC.get_theory dI
26.45 val oris = Specify.add_field' thy ppc oris
26.46 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
26.47 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
26.48 @@ -149,7 +149,7 @@
26.49 (* was fun Chead.specify *)
26.50 fun by_tactic (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ =
26.51 let (* either """"""""""""""" all empty or complete *)
26.52 - val thy = Celem.assoc_thy dI'
26.53 + val thy = ThyC.get_theory dI'
26.54 val (oris, ctxt) =
26.55 if dI' = ThyC.id_empty orelse pI' = Celem.e_pblID (*andalso? WN110511*)
26.56 then ([], ContextC.empty)
26.57 @@ -171,7 +171,7 @@
26.58 (oris, dI',pI',mI', dI, ctxt)
26.59 | _ => error "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"
26.60 val thy' = if dI = ThyC.id_empty then dI' else dI
26.61 - val thy = Celem.assoc_thy thy'
26.62 + val thy = ThyC.get_theory thy'
26.63 val {ppc, prls, where_, ...} = Specify.get_pbt pI'
26.64 val pre = Stool.check_preconds thy prls where_ pbl
26.65 val pb = foldl and_ (true, map fst pre)
26.66 @@ -213,7 +213,7 @@
26.67 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
26.68 (oris, dI', pI', mI', dI, mI, ctxt, met)
26.69 | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
26.70 - val thy = Celem.assoc_thy dI
26.71 + val thy = ThyC.get_theory dI
26.72 val (p, pt) =
26.73 case Generate.generate1 (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
26.74 ((p, Pbl), _, _, pt) => (p, pt)
26.75 @@ -229,7 +229,7 @@
26.76 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
26.77 | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
26.78 val {ppc, pre, prls,...} = Specify.get_met mID
26.79 - val thy = Celem.assoc_thy dI
26.80 + val thy = ThyC.get_theory dI
26.81 val oris = Specify.add_field' thy ppc oris
26.82 val met = if met = [] then pbl else met
26.83 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc, pre, prls) oris
26.84 @@ -245,7 +245,7 @@
26.85 | by_tactic (Tactic.Specify_Theory' domID) (pt, (p,p_)) =
26.86 let
26.87 val p_ = case p_ of Met => Met | _ => Pbl
26.88 - val thy = Celem.assoc_thy domID
26.89 + val thy = ThyC.get_theory domID
26.90 val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
26.91 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
26.92 (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
26.93 @@ -311,7 +311,7 @@
26.94 in ((pt, ([], Pbl)), []) end
26.95 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
26.96 let (* both """"""""""""""""""""""""" either empty or complete *)
26.97 - val thy = Celem.assoc_thy dI
26.98 + val thy = ThyC.get_theory dI
26.99 val (pI, (pors, pctxt), mI) =
26.100 if mI = ["no_met"]
26.101 then
27.1 --- a/src/Tools/isac/TODO.thy Wed Apr 15 16:46:41 2020 +0200
27.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 15 18:00:58 2020 +0200
27.3 @@ -152,7 +152,7 @@
27.4 \item ? what is the difference headline <--> cascmd in
27.5 Subproblem' (spec, oris, headline, fmz_, context, cascmd)
27.6 \item xxx
27.7 - \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
27.8 + \item inform: TermC.parse (ThyC.get_theory "Isac_Knowledge") istr --> parseNEW context istr
27.9 \item xxx
27.10 \item unify/clarify stac2tac_ |
27.11 \begin{itemize}
27.12 @@ -406,7 +406,7 @@
27.13 \item 1. Rewrite.eval_true_, then
27.14 LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.tac_from_prog.
27.15 \item fun associate
27.16 - let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
27.17 + let val thy = ThyC.get_theory "Isac_Knowledge";(*TODO*)
27.18 \item xxx
27.19 \item xxx
27.20 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
28.1 --- a/src/Tools/isac/Test_Code/test-code.sml Wed Apr 15 16:46:41 2020 +0200
28.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Wed Apr 15 18:00:58 2020 +0200
28.3 @@ -41,7 +41,7 @@
28.4 (case p_ of Pos.Pbl => Generate.Problem []
28.5 | Pos.Met => Generate.Method []
28.6 | _ => error "TESTg_form: uncovered case",
28.7 - Specify.itms2itemppc (Celem.assoc_thy"Isac_Knowledge") gfr pre))
28.8 + Specify.itms2itemppc (ThyC.get_theory"Isac_Knowledge") gfr pre))
28.9 end
28.10 (* for quick test-print-out, until 'type inout' is removed *)
28.11 fun f2str (Generate.FormKF cterm') = cterm'
29.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 15 16:46:41 2020 +0200
29.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 15 18:00:58 2020 +0200
29.3 @@ -135,7 +135,7 @@
29.4 "~~~~~ fun pbl2xml, args:"; val (id: pblID, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) =
29.5 (id, pbl);
29.6 "~~~~~ fun pbl2term, args:"; val (thy, (pblRD:pblRD)) = (thy, id);
29.7 -if ("Problem (" ^ (get_thy o Context.theory_name) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") =
29.8 +if ("Problem (" ^ Context.theory_name thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") =
29.9 "Problem (Pure', [e_pblID])"
29.10 then () else error "fun pbl2term changed";
29.11
30.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 16:46:41 2020 +0200
30.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 18:00:58 2020 +0200
30.3 @@ -1020,7 +1020,7 @@
30.4 "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
30.5 = (cs', (encode ifo));
30.6 val ctxt = get_ctxt pt pos (*see TODO.thy*)
30.7 - val SOME f_in = (*case*) TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr (*of*);
30.8 + val SOME f_in = (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
30.9 val f_in = Thm.term_of f_in
30.10 val pos_pred = lev_back' pos
30.11 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
30.12 @@ -1210,7 +1210,7 @@
30.13 val pos = get_pos cI 1;
30.14
30.15 "~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
30.16 - val SOME ifo = parseNEW (assoc_thy "Isac_Knowledge" |> ThyC.to_ctxt) istr
30.17 + val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) istr
30.18 val p' = lev_on p;
30.19 val tac = get_obj g_tac pt p';
30.20 val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
31.1 --- a/test/Tools/isac/Interpret/li-tool.sml Wed Apr 15 16:46:41 2020 +0200
31.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 15 18:00:58 2020 +0200
31.3 @@ -76,8 +76,8 @@
31.4
31.5 (*generate1 m (Istate.empty, ctxt) (p,p_) pt;
31.6 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
31.7 -(assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
31.8 -assoc_thy;
31.9 +(ThyC.get_theory (get_obj g_domID pt (par_pblobj pt p)));
31.10 +ThyC.get_theory;
31.11
31.12 (* ERROR which has NOT be created by this change set
31.13 (1) actual : ERROR exception PTREE "get_obj f EmptyPtree" raised (line 289 of "~~/src/Tools/isac/MathEngBasic/ctree-basic.sml")
31.14 @@ -112,7 +112,7 @@
31.15 val {srls, ...} = get_met mI;
31.16 val PblObj {meth=itms, ...} = get_obj I pt p;
31.17 val thy' = get_obj g_domID pt p;
31.18 -val thy = assoc_thy thy';
31.19 +val thy = ThyC.get_theory thy';
31.20 val srls = LItool.get_simplifier (pt, pos)
31.21 val (is as Pstate {env, ...}, ctxt, sc) = init_pstate srls ctxt itms mI;
31.22 val ini = implicit_take sc env;
31.23 @@ -200,7 +200,7 @@
31.24 Pos.on_specification p_ = false;
31.25 val pp = par_pblobj pt p
31.26 val thy' = (get_obj g_domID pt pp):ThyC.id
31.27 - val thy = assoc_thy thy'
31.28 + val thy = ThyC.get_theory thy'
31.29 val metID = get_obj g_metID pt pp
31.30 val metID' =
31.31 if metID = e_metID
31.32 @@ -312,7 +312,7 @@
31.33 (*+*)val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');
31.34 (*+*)val ctxt = get_ctxt pt''''' p''''';
31.35 (*+*)val srls = get_simplifier (pt''''', p''''');
31.36 -"~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, assoc_thy thy, meth, metID);
31.37 +"~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, ThyC.get_theory thy, meth, metID);
31.38 val (Pstate st, ctxt, Prog _) = init_pstate srls ctxt itms metID;
31.39 if pstate2str st =
31.40 "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"
32.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 15 16:46:41 2020 +0200
32.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 15 18:00:58 2020 +0200
32.3 @@ -48,7 +48,7 @@
32.4 PblObj {meth=itms, ...} => itms
32.5 | _ => error "solve Apply_Method: uncovered case get_obj"
32.6 val thy' = get_obj g_domID pt p;
32.7 - val thy = Celem.assoc_thy thy';
32.8 + val thy = ThyC.get_theory thy';
32.9 val srls = LItool.get_simplifier (pt, pos)
32.10 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
32.11 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
32.12 @@ -322,7 +322,7 @@
32.13 val Not_Associated = (*case*) associate pt ctxt (tac, stac) (*of*);
32.14 val ORundef = (*case*) or (*of*);
32.15 val Notappl "norm_equation not applicable" =
32.16 - (*case*) Applicable.applicable_in p pt (LItool.tac_from_prog pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
32.17 + (*case*) Applicable.applicable_in p pt (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") stac) (*of*);
32.18
32.19 (Term_Val1 act_arg) (* return value *);
32.20
32.21 @@ -534,7 +534,7 @@
32.22 "~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
32.23 = (ptp', (encode ifo));
32.24 val SOME f_in =
32.25 - (*case*) TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr (*of*);
32.26 + (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
32.27 val f_in = Thm.term_of f_in
32.28 val pos_pred = lev_back(*'*) pos
32.29 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
33.1 --- a/test/Tools/isac/Interpret/rewtools.sml Wed Apr 15 16:46:41 2020 +0200
33.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Wed Apr 15 18:00:58 2020 +0200
33.3 @@ -136,7 +136,7 @@
33.4 "~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite (thmID,_))) =
33.5 ((pt, pos), tac);
33.6 val Appl (Rewrite' (thy', ord', erls, _, (thmID,thm), f, (res,asm))) = applicable_in pos pt tac
33.7 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
33.8 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
33.9 val thm_deriv = Thm.get_name_hint thm;
33.10
33.11 if thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
33.12 @@ -159,7 +159,7 @@
33.13 ((pt, pos), tac);
33.14 val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =
33.15 applicable_in pos pt tac
33.16 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
33.17 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
33.18 val thm_deriv = Thm.get_name_hint thm;
33.19 if thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv) =
33.20 "thy_isac_Test-thm-risolate_bdv_add" then ()
34.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 15 16:46:41 2020 +0200
34.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 15 18:00:58 2020 +0200
34.3 @@ -157,7 +157,7 @@
34.4 PblObj {meth=itms, ...} => itms
34.5 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
34.6 val thy' = get_obj g_domID pt p;
34.7 - val thy = Celem.assoc_thy thy';
34.8 + val thy = ThyC.get_theory thy';
34.9 val srls = LItool.get_simplifier (pt, pos)
34.10 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
34.11 (is as Istate.Pstate ist, ctxt, sc) => (is, get_env ist, ctxt, sc)
34.12 @@ -236,7 +236,7 @@
34.13 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
34.14 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
34.15 val {ppc, pre, prls,...} = Specify.get_met mID
34.16 - val thy = Celem.assoc_thy dI
34.17 + val thy = ThyC.get_theory dI
34.18 val dI'' = if dI = ThyC.id_empty then dI' else dI
34.19 val pI'' = if pI = Celem.e_pblID then pI' else pI
34.20 ;
35.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Apr 15 16:46:41 2020 +0200
35.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Apr 15 18:00:58 2020 +0200
35.3 @@ -127,17 +127,17 @@
35.4 UnparseC.term tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
35.5 (* ------ ^^^ ----- ? "x" ?*)
35.6 "~~~~~ to check_leaf return val:"; val ((Program.Tac stac, a')) = ((Program.Tac (subst_atomic E t), NONE));
35.7 -val stac' = eval_prog_expr (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);
35.8 +val stac' = eval_prog_expr (ThyC.get_theory thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);
35.9 UnparseC.term stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
35.10 "~~~~~ to scan_dn return val:"; val ((a', Program.Tac stac)) = ((a', Program.Tac stac'));
35.11 -val m = LItool.tac_from_prog pt (assoc_thy th) stac;
35.12 +val m = LItool.tac_from_prog pt (ThyC.get_theory th) stac;
35.13 case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);
35.14 val (p''''', pt''''', m''''') = (p, pt, m);
35.15 "~~~~~ fun applicable_in, args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);
35.16 member op = [Pbl,Met] p_; (* = false*)
35.17 val pp = par_pblobj pt p;
35.18 val thy' = (get_obj g_domID pt pp):theory';
35.19 - val thy = assoc_thy thy'
35.20 + val thy = ThyC.get_theory thy'
35.21 val metID = (get_obj g_metID pt pp)
35.22 val {crls,...} = get_met metID
35.23 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
36.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Wed Apr 15 16:46:41 2020 +0200
36.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Wed Apr 15 18:00:58 2020 +0200
36.3 @@ -69,7 +69,7 @@
36.4 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
36.5 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
36.6 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
36.7 -val thy = if dI = ThyC.id_empty then assoc_thy dI' else assoc_thy dI;
36.8 +val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
36.9 val cpI = if pI = e_pblID then pI' else pI;
36.10 val ctxt = get_ctxt pt (p, Pbl);
36.11 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
37.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Wed Apr 15 16:46:41 2020 +0200
37.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Wed Apr 15 18:00:58 2020 +0200
37.3 @@ -69,7 +69,7 @@
37.4 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
37.5 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
37.6 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
37.7 -val thy = if dI = ThyC.id_empty then assoc_thy dI' else assoc_thy dI;
37.8 +val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
37.9 val cpI = if pI = e_pblID then pI' else pI;
37.10 val ctxt = get_ctxt pt (p, Pbl);
37.11 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
38.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 15 16:46:41 2020 +0200
38.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 15 18:00:58 2020 +0200
38.3 @@ -146,7 +146,7 @@
38.4
38.5 "~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
38.6 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
38.7 - val thy = assoc_thy dI;
38.8 + val thy = ThyC.get_theory dI;
38.9 mI = ["no_met"]; (*false*)
38.10 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
38.11 val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
38.12 @@ -169,7 +169,7 @@
38.13 "~~~~~ after fun some_spec:";
38.14 val (dI, pI, mI) = some_spec ospec spec;
38.15 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
38.16 - val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
38.17 + val thy = ThyC.get_theory dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
38.18
38.19 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
38.20 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
38.21 @@ -206,7 +206,7 @@
38.22 is wrong for simpl, but working ?!? *)
38.23 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
38.24 val pos' = ((lev_on o lev_dn) p, Frm)
38.25 - val thy = assoc_thy "Isac_Knowledge"
38.26 + val thy = ThyC.get_theory "Isac_Knowledge"
38.27 val (_,_,_,pt') = (*implicit Take*)generate1 tac_ (is, ctxt) (pt, pos');
38.28 (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');
38.29 (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
38.30 @@ -251,7 +251,7 @@
38.31 (* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
38.32 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
38.33 "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
38.34 - (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac_Knowledge"), tac_, is, pos, pt);
38.35 + (is, ctxt), (p,p_), pt) = ((ThyC.get_theory "Isac_Knowledge"), tac_, is, pos, pt);
38.36 val (pt,c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
38.37 (Rewrite thm') (f',asm) Complete;
38.38 (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
38.39 @@ -330,7 +330,7 @@
38.40 (*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);
38.41 "~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
38.42 (cs', (encode ifo));
38.43 -val SOME f_in = parse (assoc_thy "Isac_Knowledge") istr
38.44 +val SOME f_in = parse (ThyC.get_theory "Isac_Knowledge") istr
38.45 val f_in = Thm.term_of f_in
38.46 val f_succ = get_curr_formula (pt, pos);
38.47 f_succ = f_in = false;
39.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Apr 15 16:46:41 2020 +0200
39.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Apr 15 18:00:58 2020 +0200
39.3 @@ -12,7 +12,7 @@
39.4 ["Test","squ-equ-test-subpbl1"]);
39.5 "~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
39.6 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : fmz_, (dI, pI, mI) : spec) = (fmz, sp);
39.7 - val thy = assoc_thy dI;
39.8 + val thy = ThyC.get_theory dI;
39.9 (*if*) mI = ["no_met"]; (*else*)
39.10 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
39.11 val {cas, ppc, thy=thy',...} = get_pbt pI
39.12 @@ -40,7 +40,7 @@
39.13 | _ => error ""
39.14
39.15 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
39.16 - val thy = Celem.assoc_thy dI;
39.17 + val thy = ThyC.get_theory dI;
39.18 (*if*) mI = ["no_met"] = false (*else*);
39.19 val xxx = Specify.get_pbt pI
39.20 val yyy = #ppc xxx
40.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Wed Apr 15 16:46:41 2020 +0200
40.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Wed Apr 15 18:00:58 2020 +0200
40.3 @@ -50,10 +50,10 @@
40.4 pI' = e_pblID andalso pI = e_pblID; (* = false*)
40.5 find_first (is_error o #5) (pbl:itm list); (* = NONE*)
40.6
40.7 -(* nxt_add (assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl;
40.8 +(* nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl;
40.9 = SOME ("#Given", "equality (<markup> + <markup> = <markup>)") *)
40.10 "~~~~~ fun nxt_add, args:"; val (thy, oris, pbt, itms) =
40.11 - ((assoc_thy (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
40.12 + ((ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
40.13 local infix mem;
40.14 fun x mem [] = false
40.15 | x mem (y :: ys) = x = y orelse x mem ys;
41.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 15 16:46:41 2020 +0200
41.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 15 18:00:58 2020 +0200
41.3 @@ -52,7 +52,7 @@
41.4 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos);
41.5 val PblObj {meth, ctxt, ...} = get_obj I pt p;
41.6 val thy' = get_obj g_domID pt p;
41.7 -val thy = assoc_thy thy';
41.8 +val thy = ThyC.get_theory thy';
41.9 val {srls, pre, prls, ...} = get_met mI;
41.10 val pres = check_preconds thy prls pre meth |> map snd;
41.11 val ctxt = ctxt |> ContextC.insert_assumptions pres;
42.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Apr 15 16:46:41 2020 +0200
42.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Apr 15 18:00:58 2020 +0200
42.3 @@ -219,7 +219,7 @@
42.4 "~~~~~ fun tac_from_prog , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))
42.5 = (pt, (Proof_Context.theory_of ctxt), stac);
42.6 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
42.7 - val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
42.8 + val thy = Stool.common_subthy (ThyC.get_theory dI, rootthy pt);
42.9 val ags = TermC.isalist2list ags';
42.10 (*if*) mI = ["no_met"] (*else*);
42.11 val (pI, pors, mI) =
42.12 @@ -229,7 +229,7 @@
42.13 val (fmz_, vals) = Chead.oris2fmz_vals pors;
42.14 val {cas,ppc,thy,...} = Specify.get_pbt pI
42.15 val dI = Context.theory_name thy (*.take dI from _refined_ pbl.*)
42.16 - val dI = Context.theory_name (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
42.17 + val dI = Context.theory_name (Stool.common_subthy (ThyC.get_theory dI, rootthy pt));
42.18 val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> distinct);
42.19 (*\\--2 end step into relevant call ----------------------------------------------------------//*)
42.20
43.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Wed Apr 15 16:46:41 2020 +0200
43.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Wed Apr 15 18:00:58 2020 +0200
43.3 @@ -55,7 +55,7 @@
43.4 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
43.5 val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
43.6 val thy' = get_obj g_domID pt p;
43.7 - val thy = Celem.assoc_thy thy';
43.8 + val thy = ThyC.get_theory thy';
43.9 val srls = LItool.get_simplifier (pt, pos);
43.10
43.11 (*if*) mI = ["Biegelinien", "ausBelastung"] (*else*);
44.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Apr 15 16:46:41 2020 +0200
44.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Apr 15 18:00:58 2020 +0200
44.3 @@ -138,7 +138,7 @@
44.4 Generate.generate1 tac (istate, ctxt) (pt, (p', p_));
44.5 "~~~~~ fun generate1 , args:"; val (thy, (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)),
44.6 (l as (_, ctxt)), (pos as (p, p_)), pt)
44.7 - = ((Celem.assoc_thy "Isac_Knowledge"), tac, (istate, ctxt), (p', p_), pt);
44.8 + = ((ThyC.get_theory "Isac_Knowledge"), tac, (istate, ctxt), (p', p_), pt);
44.9 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
44.10 (oris, (domID, pblID, metID), hdl, ctxt_specify);
44.11
45.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Apr 15 16:46:41 2020 +0200
45.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Apr 15 18:00:58 2020 +0200
45.3 @@ -50,7 +50,7 @@
45.4 PblObj {meth=itms, ...} => itms
45.5 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
45.6 val thy' = get_obj g_domID pt p;
45.7 - val thy = Celem.assoc_thy thy';
45.8 + val thy = ThyC.get_theory thy';
45.9 val srls = LItool.get_simplifier (pt, pos)
45.10 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
45.11 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
46.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Apr 15 16:46:41 2020 +0200
46.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Apr 15 18:00:58 2020 +0200
46.3 @@ -93,7 +93,7 @@
46.4
46.5 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
46.6 val pos' = ((lev_on o lev_dn) p, Frm)
46.7 - val thy = Celem.assoc_thy "Isac_Knowledge"
46.8 + val thy = ThyC.get_theory "Isac_Knowledge"
46.9 val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *);
46.10
46.11 (** )val (_,_, (pt'', _)) =( **)
47.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 15 16:46:41 2020 +0200
47.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 15 18:00:58 2020 +0200
47.3 @@ -560,7 +560,7 @@
47.4 val sc = (#scr o get_met) metID;
47.5 val is = get_istate_LI pt (p,p_);
47.6 val thy' = get_obj g_domID pt pp;
47.7 - val thy = assoc_thy thy';
47.8 + val thy = ThyC.get_theory thy';
47.9 val d = Rule_Set.empty;
47.10 val Steps [(m',f',pt',p',c',s')] =
47.11 locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is;
48.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Wed Apr 15 16:46:41 2020 +0200
48.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Wed Apr 15 18:00:58 2020 +0200
48.3 @@ -54,7 +54,7 @@
48.4 (str2term "someTermWithBdv");
48.5 "~~~~~ fun init_istate , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
48.6 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), str2term "someTermWithBdv");
48.7 - val v = case Selem.subs2subst (Celem.assoc_thy "Isac_Knowledge") subs of
48.8 + val v = case Selem.subs2subst (ThyC.get_theory "Isac_Knowledge") subs of
48.9 (_, v) :: _ => v;
48.10 (*case*) assoc_rls rls (*of*);
48.11
49.1 --- a/test/Tools/isac/Specify/appl.sml Wed Apr 15 16:46:41 2020 +0200
49.2 +++ b/test/Tools/isac/Specify/appl.sml Wed Apr 15 18:00:58 2020 +0200
49.3 @@ -40,7 +40,7 @@
49.4 if pres = [str2term "lhs (x + 1 = 2) is_poly_in x"] then ()
49.5 else error "appl.sml Apply_Method diff.behav.";
49.6
49.7 -val ctxt = assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres;
49.8 +val ctxt = ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres;
49.9 (*TODO.WN110416 read pres from ctxt and check*)
49.10
49.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
49.12 @@ -73,7 +73,7 @@
49.13 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
49.14 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
49.15 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
49.16 -val thy = if dI = ThyC.id_empty then assoc_thy dI' else assoc_thy dI;
49.17 +val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
49.18 val cpI = if pI = e_pblID then pI' else pI;
49.19 val ctxt = get_ctxt pt (p, Pbl);
49.20 oris; (*= [(1, [1], "#Given", Const ("Input_Descript.equality", "HOL.bool...*)
50.1 --- a/test/Tools/isac/Specify/step-specify.sml Wed Apr 15 16:46:41 2020 +0200
50.2 +++ b/test/Tools/isac/Specify/step-specify.sml Wed Apr 15 18:00:58 2020 +0200
50.3 @@ -71,7 +71,7 @@
50.4 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
50.5 (*if*) pI' = Celem.e_pblID andalso pI = Celem.e_pblID (*else*);
50.6 val NONE = (*case*) find_first (is_error o #5) pbl (*of*);
50.7 - val NONE = (*case*) nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
50.8 + val NONE = (*case*) nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
50.9 (*if*) not preok (*else*);
50.10 (*if*) dI = ThyC.id_empty (*then*);
50.11