1.1 --- a/src/Tools/isac/Specify/generate.sml	Wed Mar 11 15:25:52 2020 +0100
     1.2 +++ b/src/Tools/isac/Specify/generate.sml	Tue Mar 17 14:50:19 2020 +0100
     1.3 @@ -263,45 +263,39 @@
     1.4     end
     1.5    | generate1 (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
     1.6      let
     1.7 -      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
     1.8 -      val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f 
     1.9 +      val (pt, c) = cappend_atomic pt p (is, ctxt) f 
    1.10          (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule.id_rls rls')) (f', asm) Complete
    1.11        val pt = update_branch pt p TransitiveB
    1.12      in
    1.13        ((p, Res), c, FormKF (Rule.term2str f'), pt)
    1.14      end
    1.15 -  | generate1 (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (pt, (p, _)) =
    1.16 +  | generate1 (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, _)) (is, ctxt) (pt, (p, _)) =
    1.17      let
    1.18 -      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
    1.19 -      val ctxt' = ContextC.insert_assumptions asm ctxt
    1.20 -      val (pt, _) = cappend_form pt p (is, ctxt') f 
    1.21 +      val (pt, _) = cappend_form pt p (is, ctxt) f 
    1.22        val pt = update_branch pt p TransitiveB
    1.23        val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule.id_rls rls)) f 
    1.24 -      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt')
    1.25 +      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt)
    1.26        val pos' = ((lev_on o lev_dn) p, Frm)
    1.27      in
    1.28 -      generate1 tac_ (is, ctxt') (pt, pos') (*implicit Take*)
    1.29 +      generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
    1.30      end
    1.31    | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
    1.32      let
    1.33 -      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
    1.34 -      val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f 
    1.35 -        (Tactic.Rewrite_Set (Rule.id_rls rls')) (f',asm) Complete
    1.36 +      val (pt, c) = cappend_atomic pt p (is, ctxt) f 
    1.37 +        (Tactic.Rewrite_Set (Rule.id_rls rls')) (f', asm) Complete
    1.38        val pt = update_branch pt p TransitiveB
    1.39      in
    1.40        ((p, Res), c, FormKF (Rule.term2str f'), pt)
    1.41      end
    1.42 -  | generate1 (Tactic.Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (pt, (p, _)) =
    1.43 +  | generate1 (Tactic.Detail_Set' (_, _, rls, f, _)) (is, ctxt) (pt, (p, _)) =
    1.44      let
    1.45 -      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
    1.46 -      val ctxt' = ContextC.insert_assumptions asm ctxt
    1.47 -      val (pt, _) = cappend_form pt p (is, ctxt') f 
    1.48 +      val (pt, _) = cappend_form pt p (is, ctxt) f 
    1.49        val pt = update_branch pt p TransitiveB
    1.50        val is = init_istate (Tactic.Rewrite_Set (Rule.id_rls rls)) f
    1.51 -      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt')
    1.52 +      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt)
    1.53        val pos' = ((lev_on o lev_dn) p, Frm)
    1.54      in
    1.55 -      generate1 tac_ (is, ctxt') (pt, pos') (*implicit Take*)
    1.56 +      generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
    1.57      end
    1.58    | generate1 (Tactic.Check_Postcond' (_, (scval, asm))) l (pt, (p, _)) =
    1.59        let
    1.60 @@ -355,16 +349,14 @@
    1.61      val f = get_curr_formula (pt, pos)
    1.62      val pos' as (p', _) = (lev_on p, Res)
    1.63      val (pt, _) = case subs_opt of
    1.64 -      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
    1.65 -      NONE => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
    1.66 +      NONE => cappend_atomic pt p' (is, ctxt) f
    1.67          (Tactic.Rewrite thm') (f', []) Inconsistent
    1.68 -      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
    1.69 -    | SOME subs => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
    1.70 +    | SOME subs => cappend_atomic pt p' (is, ctxt) f
    1.71          (Tactic.Rewrite_Inst (subs, thm')) (f', []) Inconsistent
    1.72      val pt = update_branch pt p' TransitiveB
    1.73    in (pt, pos') end
    1.74  
    1.75 -fun generate_hard thy m' (p,p_) pt =
    1.76 +fun generate_hard _(*thy*) m' (p,p_) pt =
    1.77    let  
    1.78      val p = case p_ of
    1.79        Frm => p | Res => lev_on p

     2.1 --- a/src/Tools/isac/TODO.thy	Wed Mar 11 15:25:52 2020 +0100
     2.2 +++ b/src/Tools/isac/TODO.thy	Tue Mar 17 14:50:19 2020 +0100
     2.3 @@ -143,6 +143,7 @@
     2.4    \item xxx
     2.5    \item generate, generate1: NO thy as arg.
     2.6          Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
     2.7 +        redesign return value (originally for output by fun me?)
     2.8    \item xxx
     2.9    \item shift tests into NEW model.sml (upd, upds_envv, ..)
    2.10    \item xxx
    2.11 @@ -157,7 +158,7 @@
    2.12        rm Assumptions  :: bool  (* TODO: remove with making ^^^ idle *)
    2.13      \item xxx
    2.14      \item xxx
    2.15 -    \item remove ctxt from Tactic.T; this makes use of ctxt more explicit (e.g. in LI)
    2.16 +    \item remove ctxt from Tactic.Subproblem'; this makes use of ctxt more explicit (e.g. in LI)
    2.17        \begin{itemize}
    2.18        \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
    2.19        \item rm ctxt from Subproblem' (is separated in associate!))