diff -r 7601a1fa20b9 -r d2be99d0bf1e src/Tools/isac/Interpret/solve-step.sml
--- a/src/Tools/isac/Interpret/solve-step.sml	Sat May 02 15:41:27 2020 +0200
+++ b/src/Tools/isac/Interpret/solve-step.sml	Sat May 02 16:34:42 2020 +0200
@@ -34,7 +34,7 @@
     	    case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
     	      SOME (f', (id, thm))
     	        => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
-    	    | NONE => Applicable.No ("'calculate "^op_^"' not applicable") 
+    	    | NONE => Applicable.No ("'calculate " ^ op_ ^ "' not applicable") 
         else Applicable.No msg                                              
       end
   | check (Tactic.Check_Postcond pI) (_, _) = (*TODO: only applicable, if evaluating to True*)
@@ -46,47 +46,40 @@
         Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, [])))
       end
   | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
-  | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')        (* always applicable *)
-  | check Tactic.Or_to_List (pt, (p, p_)) =
+  | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')
+  | check Tactic.Or_to_List cs =
        let 
-        val f = case p_ of
-          Pos.Frm => Ctree.get_obj Ctree.g_form pt p
-    	  | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
-        | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
-      in (let val ls = Prog_Expr.or2list f
-          in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end) 
-         handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)
+        val f = Calc.current_formula cs;
+        val ls = Prog_Expr.or2list f;
+      in
+        Applicable.Yes (Tactic.Or_to_List' (f, ls))
       end
-  | check (Tactic.Rewrite thm'') (cs as (pt, (p, _))) = 
+  | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) = 
       let
-        val (msg, thy', ro, rls', _)= ApplicableOLD.from_pblobj_or_detail_thm thm'' p pt;
+        val (msg, thy', ro, rls', _) = ApplicableOLD.from_pblobj_or_detail_thm thm p pt;
         val thy = ThyC.get_theory thy';
         val f = Calc.current_formula cs;
       in
         if msg = "OK" 
         then
-          case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
-            SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
-          | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable") 
+          case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm) f of
+            SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
+          | NONE => Applicable.No ((thm |> fst |> quote) ^ " not applicable") 
         else Applicable.No msg
       end
-  | check (Tactic.Rewrite_Inst (subs, thm'')) (cs as (pt, (p, _))) = 
+  | check (Tactic.Rewrite_Inst (subs, thm)) (cs as (pt, (p, _))) = 
       let 
         val pp = Ctree.par_pblobj pt p;
         val thy' = Ctree.get_obj Ctree.g_domID pt pp;
         val thy = ThyC.get_theory thy';
         val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
         val f = Calc.current_formula cs;
+        val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
       in 
-        let
-          val subst = Subst.T_from_input thy subs;
-        in
-          case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of
-            SOME (f',asm) =>
-              Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
-          | NONE => Applicable.No ((fst thm'')^" not applicable")
-        end
-        handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
+        case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm) f of
+          SOME (f', asm) =>
+            Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
+        | NONE => Applicable.No (fst thm ^ " not applicable")
       end
   | check (Tactic.Rewrite_Set rls) (cs as (pt, (p, _))) =
       let 
@@ -99,37 +92,29 @@
             => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
           | NONE => Applicable.No (rls ^ " not applicable")
       end
-  | check (m as Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, p_))) =
-    if member op = [Pos.Pbl, Pos.Met] p_ 
-    then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
-    else
+  | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, (p, _))) =
       let 
         val pp = Ctree.par_pblobj pt p;
         val thy' = Ctree.get_obj Ctree.g_domID pt pp;
         val thy = ThyC.get_theory thy';
         val f = Calc.current_formula cs;
-    	  val subst = Subst.T_from_input thy subs;
+    	  val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
       in 
         case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
           SOME (f', asm)
             => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
         | NONE => Applicable.No (rls ^ " not applicable")
-        handle _ => Applicable.No ("syntax error in " ^(subs2str subs))
       end
   | check (Tactic.Subproblem (domID, pblID)) (_, _) = 
       Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [], 
 			  TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
- 
-   (*Substitute combines two different kind of "substitution":
-      (1) subst_atomic: for ?a..?z
-      (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
-  | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
+   | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
       let
         val pp = Ctree.par_pblobj pt p
         val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
         val f = Calc.current_formula cs;
 		    val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
-		    val subte = Subst.input_to_terms sube
+		    val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
 		    val subst = Subst.T_from_string_eqs thy sube
 		    val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
 		  in
@@ -146,37 +131,30 @@
 		      | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
 		  end
   | check (Tactic.Tac id) (cs as (pt, (p, _))) =
-    let 
-      val pp = Ctree.par_pblobj pt p; 
-      val thy' = Ctree.get_obj Ctree.g_domID pt pp;
-      val thy = ThyC.get_theory thy';
-      val f = Calc.current_formula cs;
-    in case id of
-      "subproblem_equation_dummy" =>
-  	  if TermC.is_expliceq f
-  	  then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
-  	  else Applicable.No "applicable only to equations made explicit"
-    | "solve_equation_dummy" =>
-  	  let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);
-  	  in
-  	    if id' <> "subproblem_equation_dummy"
-  	    then Applicable.No "no subproblem"
-  	    else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
-  		    then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
-  		    else error ("Solve_Step.check: f= " ^ f')
+      let 
+        val pp = Ctree.par_pblobj pt p; 
+        val thy' = Ctree.get_obj Ctree.g_domID pt pp;
+        val thy = ThyC.get_theory thy';
+        val f = Calc.current_formula cs;
+      in case id of
+        "subproblem_equation_dummy" =>
+    	  if TermC.is_expliceq f
+    	  then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
+    	  else Applicable.No "applicable only to equations made explicit"
+      | "solve_equation_dummy" =>
+    	  let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);
+    	  in
+    	    if id' <> "subproblem_equation_dummy"
+    	    then Applicable.No "no subproblem"
+    	    else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
+    		    then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
+    		    else error ("Solve_Step.check: f= " ^ f')
+        end
+      | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
       end
-    | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
-    end
   | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
-  | check (Tactic.Begin_Trans) (pt, (p, p_)) =
-    let
-      val (f, _) = case p_ of   (*p 12.4.00 unnecessary, implizit Take in gen*)
-        Pos.Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)
-      | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p)
-      | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
-    in (Applicable.Yes (Tactic.Begin_Trans' f))
-      handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds  syntaxerror in '" ^ UnparseC.term f ^ "'")
-    end
+  | check (Tactic.Begin_Trans) cs =
+      Applicable.Yes (Tactic.Begin_Trans' (Calc.current_formula cs))
   | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
     if p_ = Pos.Res 
 	  then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))