diff -r cc5b51681c4b -r 87336f3b021f src/Tools/isac/Interpret/solve-step.sml
--- a/src/Tools/isac/Interpret/solve-step.sml	Sat May 02 17:39:04 2020 +0200
+++ b/src/Tools/isac/Interpret/solve-step.sml	Mon May 04 09:25:51 2020 +0200
@@ -9,6 +9,10 @@
 sig
   val check: Tactic.input -> Calc.T -> Applicable.T
   val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
+  val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
+  val s_add_general: State_Steps.T ->
+    Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
+
 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
   (*NONE*)                                                     
 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
@@ -25,7 +29,20 @@
   check tactics (input by the user, mostly) for applicability
   and determine as much of the result of the tactic as possible initially.
 *)
-fun check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
+fun check (Tactic.Apply_Method mI) (pt, (p, _)) =
+      let
+        val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
+          Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
+        | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
+        val {where_, ...} = Specify.get_pbt pI
+        val pres = map (Model.mk_env probl |> subst_atomic) where_
+        val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
+          then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
+          else ctxt
+      in
+        Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
+      end
+  | check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
       let 
         val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
         val f = Calc.current_formula cs;
@@ -163,7 +180,13 @@
   | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
   | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
 
-fun add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
+fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) = 
+    (case topt of 
+      SOME t => 
+        let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
+        in (pos, c, Generate.EmptyMout, pt) end
+    | NONE => (pos, [], Generate.EmptyMout, pt))
+  | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
     let
       val p =
         let val (ps, p') = split_last p (* no connex to prev.ppobj *)
@@ -261,13 +284,31 @@
       end
   | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))
       (l as (_, ctxt)) (pt, (p, _)) =
+      let
+  	    val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
+  	      (oris, (domID, pblID, metID), hdl, ctxt_specify)
+  	    val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
+      in
+        ((p, Pos.Pbl), c, Generate.FormKF f, pt)
+      end
+  | add m' _ (_, pos) =
+      raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
+
+(* LI switches between solve-phase and specify-phase *)
+fun add_general tac ic cs =
+  if Tactic.for_specify' tac
+  then Generate.generate1 tac ic cs
+  else add tac ic cs
+
+(* tacis are in reverse order from do_next/specify_: last = fst to insert *)
+fun s_add_general [] ptp = ptp
+  | s_add_general tacis (pt, c, _) = 
     let
-	    val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
-	      (oris, (domID, pblID, metID), hdl, ctxt_specify)
-	    val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
+      val (tacis', (_, tac_, (p, is))) = split_last tacis
+	    val (p',c',_,pt') = add_general tac_ is (pt, p)
     in
-      ((p, Pos.Pbl), c, Generate.FormKF f, pt)
+      s_add_general tacis' (pt', c@c', p')
     end
-  | add m' _ _ = raise ERROR ("add: not impl.for " ^ Tactic.string_of m')
+
 
 (**)end(**);