1.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Sat May 02 11:36:13 2020 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Sat May 02 12:13:20 2020 +0200
     1.3 @@ -67,19 +67,15 @@
     1.4        in
     1.5          Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))
     1.6        end
     1.7 -(*RM* )| Derive of Rule_Set.id( *RM*)
     1.8    | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
     1.9    | check (Tactic.Free_Solve) _ = Applicable.Yes (Tactic.Free_Solve')        (* always applicable *)
    1.10 -  | check  (Tactic.Apply_Assumption cts') _ =
    1.11 -    raise ERROR ("Solve_Step.check: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
    1.12 -    (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
    1.13    | check Tactic.Or_to_List (pt, (p, p_)) =
    1.14      if member op = [Pos.Pbl, Pos.Met] p_ 
    1.15      then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_)))
    1.16      else
    1.17        let 
    1.18          val f = case p_ of
    1.19 -          Frm => Ctree.get_obj Ctree.g_form pt p
    1.20 +          Pos.Frm => Ctree.get_obj Ctree.g_form pt p
    1.21      	  | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
    1.22          | _ => error ("Solve_Step.check: call by " ^ Pos.pos'2str (p, p_));
    1.23        in (let val ls = Prog_Expr.or2list f