# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1584453019 -3600
# Node ID 6638657645a302ff04f06831ec3599eef75f946f
# Parent  168abe8dd1e39fd5775b04f70bbb3d3e46961bb6
clean ctxt handling: remove double insert_assumptions

diff -r 168abe8dd1e3 -r 6638657645a3 src/Tools/isac/Specify/generate.sml
--- a/src/Tools/isac/Specify/generate.sml	Wed Mar 11 15:25:52 2020 +0100
+++ b/src/Tools/isac/Specify/generate.sml	Tue Mar 17 14:50:19 2020 +0100
@@ -263,45 +263,39 @@
    end
   | generate1 (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
     let
-      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
-      val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f 
+      val (pt, c) = cappend_atomic pt p (is, ctxt) f 
         (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule.id_rls rls')) (f', asm) Complete
       val pt = update_branch pt p TransitiveB
     in
       ((p, Res), c, FormKF (Rule.term2str f'), pt)
     end
-  | generate1 (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (pt, (p, _)) =
+  | generate1 (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, _)) (is, ctxt) (pt, (p, _)) =
     let
-      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
-      val ctxt' = ContextC.insert_assumptions asm ctxt
-      val (pt, _) = cappend_form pt p (is, ctxt') f 
+      val (pt, _) = cappend_form pt p (is, ctxt) f 
       val pt = update_branch pt p TransitiveB
       val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule.id_rls rls)) f 
-      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt')
+      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt)
       val pos' = ((lev_on o lev_dn) p, Frm)
     in
-      generate1 tac_ (is, ctxt') (pt, pos') (*implicit Take*)
+      generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
     end
   | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
     let
-      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
-      val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f 
-        (Tactic.Rewrite_Set (Rule.id_rls rls')) (f',asm) Complete
+      val (pt, c) = cappend_atomic pt p (is, ctxt) f 
+        (Tactic.Rewrite_Set (Rule.id_rls rls')) (f', asm) Complete
       val pt = update_branch pt p TransitiveB
     in
       ((p, Res), c, FormKF (Rule.term2str f'), pt)
     end
-  | generate1 (Tactic.Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (pt, (p, _)) =
+  | generate1 (Tactic.Detail_Set' (_, _, rls, f, _)) (is, ctxt) (pt, (p, _)) =
     let
-      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
-      val ctxt' = ContextC.insert_assumptions asm ctxt
-      val (pt, _) = cappend_form pt p (is, ctxt') f 
+      val (pt, _) = cappend_form pt p (is, ctxt) f 
       val pt = update_branch pt p TransitiveB
       val is = init_istate (Tactic.Rewrite_Set (Rule.id_rls rls)) f
-      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt')
+      val tac_ = Tactic.Apply_Method' (Celem.e_metID, SOME Rule.e_term (*t ..has not been declared*), is, ctxt)
       val pos' = ((lev_on o lev_dn) p, Frm)
     in
-      generate1 tac_ (is, ctxt') (pt, pos') (*implicit Take*)
+      generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*)
     end
   | generate1 (Tactic.Check_Postcond' (_, (scval, asm))) l (pt, (p, _)) =
       let
@@ -355,16 +349,14 @@
     val f = get_curr_formula (pt, pos)
     val pos' as (p', _) = (lev_on p, Res)
     val (pt, _) = case subs_opt of
-      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
-      NONE => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
+      NONE => cappend_atomic pt p' (is, ctxt) f
         (Tactic.Rewrite thm') (f', []) Inconsistent
-      (*ctxt updated by locate_input_tactic &TODO;vvv insert_assumptions is LEGACY vvv *)
-    | SOME subs => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f
+    | SOME subs => cappend_atomic pt p' (is, ctxt) f
         (Tactic.Rewrite_Inst (subs, thm')) (f', []) Inconsistent
     val pt = update_branch pt p' TransitiveB
   in (pt, pos') end
 
-fun generate_hard thy m' (p,p_) pt =
+fun generate_hard _(*thy*) m' (p,p_) pt =
   let  
     val p = case p_ of
       Frm => p | Res => lev_on p
diff -r 168abe8dd1e3 -r 6638657645a3 src/Tools/isac/TODO.thy
--- a/src/Tools/isac/TODO.thy	Wed Mar 11 15:25:52 2020 +0100
+++ b/src/Tools/isac/TODO.thy	Tue Mar 17 14:50:19 2020 +0100
@@ -143,6 +143,7 @@
   \item xxx
   \item generate, generate1: NO thy as arg.
         Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
+        redesign return value (originally for output by fun me?)
   \item xxx
   \item shift tests into NEW model.sml (upd, upds_envv, ..)
   \item xxx
@@ -157,7 +158,7 @@
       rm Assumptions  :: bool  (* TODO: remove with making ^^^ idle *)
     \item xxx
     \item xxx
-    \item remove ctxt from Tactic.T; this makes use of ctxt more explicit (e.g. in LI)
+    \item remove ctxt from Tactic.Subproblem'; this makes use of ctxt more explicit (e.g. in LI)
       \begin{itemize}
       \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
       \item rm ctxt from Subproblem' (is separated in associate!))