1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Mon May 04 12:38:16 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Mon May 04 13:27:45 2020 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4    | check (Tactic.Subproblem (domID, pblID)) (_, _) = 
     1.5        Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [], 
     1.6  			  TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
     1.7 -   | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
     1.8 +  | check (Tactic.Substitute sube) (cs as (pt, (p, _))) =
     1.9        let
    1.10          val pp = Ctree.par_pblobj pt p
    1.11          val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
    1.12 @@ -218,21 +218,8 @@
    1.13          val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.14          val thy = ThyC.get_theory thy';
    1.15          val f = Calc.current_formula cs;
    1.16 -      in case id of
    1.17 -        "subproblem_equation_dummy" =>
    1.18 -    	  if TermC.is_expliceq f
    1.19 -    	  then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
    1.20 -    	  else Applicable.No "applicable only to equations made explicit"
    1.21 -      | "solve_equation_dummy" =>
    1.22 -    	  let val (id', f') = ApplicableOLD.split_dummy (UnparseC.term f);
    1.23 -    	  in
    1.24 -    	    if id' <> "subproblem_equation_dummy"
    1.25 -    	    then Applicable.No "no subproblem"
    1.26 -    	    else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
    1.27 -    		    then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
    1.28 -    		    else error ("Solve_Step.check: f= " ^ f')
    1.29 -        end
    1.30 -      | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
    1.31 +      in
    1.32 +        Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
    1.33        end
    1.34    | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
    1.35    | check (Tactic.Begin_Trans) cs =