# HG changeset patch
# User wneuper <Walther.Neuper@jku.at>
# Date 1673177607 -3600
# Node ID 2fca46ba633a7d2a3e62a2832134f2496e19c229
# Parent  c4f68c7bbbfc4873d70696f43ddf26390c98df47
eliminate use of Thy_Info 4: ThyC.get_theory in Step_Solve, Fetch_Tacs

diff -r c4f68c7bbbfc -r 2fca46ba633a src/Tools/isac/Interpret/step-solve.sml
--- a/src/Tools/isac/Interpret/step-solve.sml	Sun Jan 08 10:30:58 2023 +0100
+++ b/src/Tools/isac/Interpret/step-solve.sml	Sun Jan 08 12:33:27 2023 +0100
@@ -36,45 +36,46 @@
       ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
     end
   | by_tactic m (pt, po as (p, p_)) =
-    if MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
-    then
-      let
-        val ctxt = get_ctxt pt po
-        val ((p, p_), ps, _, pt) = Solve_Step.add_general m (Istate.empty, ctxt) (pt, (p, p_))
-	    in ("no-method-specified", (*Free_Solve*)
-	      ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))
-      end
-    else
-	    let 
-	      val (is, sc) = LItool.resume_prog (p,p_) pt;
-	    in
-        case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
-          LI.Safe_Step (istate, ctxt, tac) =>
-            let
-               val p' = next_in_prog po
-               val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_))
-            in
-       		    ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
-                [(*Ctree NOT cut*)], (pt', p'')))
+    let
+      val ctxt = get_ctxt pt po
+      val thy = Proof_Context.theory_of ctxt
+    in
+      if MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
+      then
+        let val ((p, p_), ps, _, pt) = Solve_Step.add_general m (Istate.empty, ctxt) (pt, (p, p_))
+  	    in ("no-method-specified", (*Free_Solve*)
+  	      ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))
+        end
+      else
+  	    let val (is, sc) = LItool.resume_prog (p,p_) pt;
+  	    in
+          case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
+            LI.Safe_Step (istate, ctxt, tac) =>
+              let
+                 val p' = next_in_prog po
+                 val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_))
+              in
+         		    ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
+                  [(*Ctree NOT cut*)], (pt', p'')))
+              end
+  	      | LI.Unsafe_Step (istate, ctxt, tac) =>
+              let
+                 val p' = 
+                   case p_ of Frm => p 
+                   | Res => lev_on p
+                   | _ => raise ERROR ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));
+                 val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_));
+              in
+         		    ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
+                  [(*Ctree NOT cut*)], (pt', p'')))
+              end
+  	      | _ => (* NotLocatable *)
+  	        let val (p,ps, _, pt) = Solve_Step.add_hard thy m (p, p_) pt;
+  	        in
+  	          ("not-found-in-program", ([(Tactic.input_from_T ContextC.empty m, m, (po, is))], ps, (pt, p)))
             end
-	      | LI.Unsafe_Step (istate, ctxt, tac) =>
-            let
-               val p' = 
-                 case p_ of Frm => p 
-                 | Res => lev_on p
-                 | _ => raise ERROR ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));
-               val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_));
-            in
-       		    ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
-                [(*Ctree NOT cut*)], (pt', p'')))
-            end
-	      | _ => (* NotLocatable *)
-	        let 
-	          val (p,ps, _, pt) = Solve_Step.add_hard (ThyC.get_theory "Isac_Knowledge") m (p, p_) pt;
-	        in
-	          ("not-found-in-program", ([(Tactic.input_from_T ContextC.empty m, m, (po, is))], ps, (pt, p)))
-          end
-	    end;
+  	    end
+    end;
 
 val do_next = LI.do_next
 
diff -r c4f68c7bbbfc -r 2fca46ba633a src/Tools/isac/MathEngine/fetch-tactics.sml
--- a/src/Tools/isac/MathEngine/fetch-tactics.sml	Sun Jan 08 10:30:58 2023 +0100
+++ b/src/Tools/isac/MathEngine/fetch-tactics.sml	Sun Jan 08 12:33:27 2023 +0100
@@ -27,12 +27,11 @@
     else
       let
         val pp = par_pblobj pt p;
-        val thy' = get_obj g_domID pt pp;
-        val thy = ThyC.get_theory thy';
         val ctxt = Ctree.get_ctxt pt pos
-        val metID = get_obj g_metID pt pp;
-        val metID' = if metID = MethodC.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
-        val (sc, prog_rls) = (case MethodC.from_store ctxt metID' of
+        val met_id = get_obj g_metID pt pp;
+        val met_id_ori = (thd3 o snd3) (get_obj g_origin pt pp)
+        val met_id' = if met_id = MethodC.id_empty then met_id_ori else met_id
+        val (sc, prog_rls) = (case MethodC.from_store ctxt met_id' of
             {program = Rule.Prog sc, prog_rls, ...} => (sc, prog_rls) | _ => raise ERROR "from_prog 1")
         val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
         val ctxt = get_ctxt pt (p, p_)
@@ -51,8 +50,6 @@
       let
         val pp = par_pblobj pt p       
         val ctxt = Ctree.get_loc pt pos |> snd
-        val thy = Ctree.get_loc pt pos |> snd |> Proof_Context.theory_of
-
         val metID = get_obj g_metID pt pp
         val metID' =
           if metID = MethodC.id_empty