1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Sat May 02 09:15:39 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Sat May 02 10:57:04 2020 +0200
     1.3 @@ -231,10 +231,6 @@
     1.4      | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
     1.5      end
     1.6    | check (Tactic.Take str) _ = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
     1.7 -(*RM*)| check (Tactic.Take_Inst ct') _ =
     1.8 -    raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))
     1.9 -(*RM*)| check (Tactic.Begin_Sequ) _ =
    1.10 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
    1.11    | check (Tactic.Begin_Trans) (pt, (p, p_)) =
    1.12      let
    1.13        val (f, _) = case p_ of   (*p 12.4.00 unnecessary, implizit Take in gen*)
    1.14 @@ -244,65 +240,10 @@
    1.15      in (Applicable.Yes (Tactic.Begin_Trans' f))
    1.16        handle _ => raise ERROR ("Solve_Step.check: Begin_Trans finds  syntaxerror in '" ^ UnparseC.term f ^ "'")
    1.17      end
    1.18 -  | check (Tactic.Split_And) _ =
    1.19 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)
    1.20 -  | check (Tactic.Split_Or) _ =
    1.21 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)
    1.22 -  | check (Tactic.Split_Intersect) _ =
    1.23 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))
    1.24 -  | check (Tactic.Conclude_And) _ =
    1.25 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)
    1.26 -  | check (Tactic.Conclude_Or) _ =
    1.27 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)
    1.28 -  | check Tactic.Collect_Trues _ =
    1.29 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
    1.30 -  | check (Tactic.End_Sequ) _ =
    1.31 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))
    1.32    | check (Tactic.End_Trans) (pt, (p, p_)) = (*TODO: check parent branches*)
    1.33      if p_ = Pos.Res 
    1.34  	  then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
    1.35      else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
    1.36 -  | check Tactic.End_Ruleset _ = raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
    1.37 -  | check (Tactic.End_Subproblem) _ =
    1.38 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
    1.39 -  | check (Tactic.End_Intersect) _ =
    1.40 -    error ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
    1.41 -  | check (m as Tactic.Detail_Set rls) (pt, (p, p_)) =
    1.42 -    if member op = [Pos.Pbl, Pos.Met] p_ 
    1.43 -    then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
    1.44 -    else
    1.45 -    	let
    1.46 -    	  val pp = Ctree.par_pblobj pt p 
    1.47 -    	  val thy' = Ctree.get_obj Ctree.g_domID pt pp
    1.48 -    	  val f = case p_ of
    1.49 -    			Frm => Ctree.get_obj Ctree.g_form pt p
    1.50 -    		| Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
    1.51 -    		| _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
    1.52 -    	in
    1.53 -    	  case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
    1.54 -    	    SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
    1.55 -    	  | NONE => Applicable.No (rls^" not applicable")
    1.56 -    	end
    1.57 -  | check (m as Tactic.Detail_Set_Inst (subs, rls)) (pt, (p, p_)) = 
    1.58 -    if member op = [Pos.Pbl, Pos.Met] p_ 
    1.59 -    then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
    1.60 -    else
    1.61 -      let 
    1.62 -        val pp = Ctree.par_pblobj pt p;
    1.63 -        val thy' = Ctree.get_obj Ctree.g_domID pt pp;
    1.64 -        val thy = ThyC.get_theory thy';
    1.65 -        val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p
    1.66 -    		| Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
    1.67 -    		| _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
    1.68 -        val subst = Subst.T_from_input thy subs
    1.69 -      in 
    1.70 -        case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
    1.71 -          SOME (f', asm)
    1.72 -            => Applicable.Yes (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
    1.73 -        | NONE => Applicable.No (rls ^ " not applicable")
    1.74 -        handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
    1.75 -      end
    1.76 -(*RM* )| End_Detail( *RM*)
    1.77    | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
    1.78    | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
    1.79