1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Thu Jan 26 13:31:07 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Thu Jan 26 18:54:25 2023 +0100
     1.3 @@ -333,7 +333,7 @@
     1.4        1 + count_kestore_ptyps ps  + count_kestore_ptyps ps';
     1.5  fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
     1.6        (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
     1.7 -val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
     1.8 +fun check_kestore_ptyp ctxt ptyp = check_kestore_ptyp' (Probl_Def.s_to_string ctxt) ptyp;
     1.9  fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
    1.10  fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
    1.11  fun sort_kestore_ptyp' _ [] = []

     2.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml	Thu Jan 26 13:31:07 2023 +0100
     2.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml	Thu Jan 26 18:54:25 2023 +0100
     2.3 @@ -11,8 +11,7 @@
     2.4  sig
     2.5    type T
     2.6    type single
     2.7 -  val to_string: single list -> string
     2.8 -  val to_string_PIDE: Proof.context -> single list -> string
     2.9 +  val to_string: Proof.context -> single list -> string
    2.10  
    2.11    type model_input_pos
    2.12    type pre_model
    2.13 @@ -37,7 +36,6 @@
    2.14      m_field * term * Position.T
    2.15    val parse_pattern: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) ->
    2.16      m_field * term * Position.T
    2.17 -  val to_string': T -> string
    2.18  \<close>
    2.19  end
    2.20  
    2.21 @@ -95,15 +93,12 @@
    2.22        |> map (fn (_, a, b) => (a, b))
    2.23    in (model, where_) end
    2.24  
    2.25 -fun pat2str (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id));
    2.26 -fun to_string pats = (strs2str o (map pat2str)) pats;
    2.27 -fun pat2str_PIDE ctxt (field, (dsc, id)) =
    2.28 +fun pat2str ctxt (field, (dsc, id)) =
    2.29    pair2str (field, pair2str (UnparseC.term_in_ctxt ctxt dsc, UnparseC.term_in_ctxt ctxt id));
    2.30 -fun to_string_PIDE ctxt pats = (strs2str o (map (pat2str_PIDE ctxt))) pats;
    2.31 +fun to_string ctxt pats = (strs2str o (map (pat2str ctxt))) pats;
    2.32  
    2.33  \<^isac_test>\<open>
    2.34 -fun pat2str' (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id)) ^ "\n";
    2.35 -fun to_string' pats = (strs2str o (map pat2str')) pats;
    2.36 +(**)
    2.37  \<close>
    2.38  
    2.39  (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)

     3.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml	Thu Jan 26 13:31:07 2023 +0100
     3.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml	Thu Jan 26 18:54:25 2023 +0100
     3.3 @@ -18,7 +18,7 @@
     3.4    val empty_store: T Store.node
     3.5  
     3.6    val check_unique: Check_Unique.id -> T Store.T -> unit
     3.7 -  val s_to_string: T list -> string
     3.8 +  val s_to_string: Proof.context -> T list -> string
     3.9  end
    3.10  
    3.11  (**)
    3.12 @@ -47,14 +47,15 @@
    3.13  }   
    3.14  val empty = {guh = "pbl_empty", mathauthors = [], start_refine = id_empty, thy = @{theory "Pure"},
    3.15    cas = NONE, where_rls = Rule_Set.Empty, where_ = [], model = [], solve_mets = []} : T
    3.16 -fun pbt2str ({cas = cas', guh = guh', start_refine = init', mathauthors = ma', solve_mets = met', model = model',
    3.17 -      where_rls = prls', thy = thy', where_ = w'} : T)
    3.18 -    = "{cas = " ^ (UnparseC.term_opt cas') ^  ", guh = \"" ^ guh'  ^ "\", start_refine = "
    3.19 -      ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", solve_mets = "
    3.20 -      ^ (strslist2strs met') ^ ", model = " ^ Model_Pattern.to_string model' ^ ", where_rls = "
    3.21 -      ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
    3.22 -      ^ (UnparseC.terms w') ^ "}" |> linefeed;
    3.23 -fun s_to_string pbts = map pbt2str pbts |> list2str;
    3.24 +
    3.25 +fun pbt2str ctxt {cas = cas', guh = guh', start_refine = init', mathauthors = ma',
    3.26 +      solve_mets = met', model = model', where_rls = prls', thy = thy', where_ = w'} =
    3.27 +  "{cas = " ^ UnparseC.term_opt cas' ^  ", guh = \"" ^ guh'  ^ "\", start_refine = "
    3.28 +  ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", solve_mets = "
    3.29 +  ^ (strslist2strs met') ^ ", model = " ^ Model_Pattern.to_string ctxt model' ^ ", where_rls = "
    3.30 +  ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
    3.31 +  ^ (UnparseC.terms_in_ctxt ctxt w') ^ "}" |> linefeed;
    3.32 +fun s_to_string ctxt pbts = map (pbt2str ctxt) pbts |> list2str;
    3.33  
    3.34  val empty_store = Store.Node ("empty_probl_id", [empty], [])
    3.35  type store = (T Store.node) list

     4.1 --- a/src/Tools/isac/Interpret/derive.sml	Thu Jan 26 13:31:07 2023 +0100
     4.2 +++ b/src/Tools/isac/Interpret/derive.sml	Thu Jan 26 18:54:25 2023 +0100
     4.3 @@ -143,10 +143,10 @@
     4.4    (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj
     4.5      and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
     4.6      let
     4.7 -      val (res, asm) = (State_Steps.result o last_elem) tacis
     4.8      	val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
     4.9      	  (SOME (ist, ctxt), _) => (ist, ctxt)
    4.10        | (NONE, _) => raise ERROR "Derive.embed Frm: uncovered case get_obj"
    4.11 +      val (res, asm) = ((State_Steps.result ctxt) o last_elem) tacis
    4.12      	val form =  Ctree.get_obj  Ctree.g_form pt p
    4.13        (*val p = lev_on p; ---------------only difference to (..,Res) below*)
    4.14      	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
    4.15 @@ -161,10 +161,10 @@
    4.16      (*inform at Res: append a Transitive-PrfObj
    4.17        and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
    4.18      let
    4.19 -      val (res, asm) = (State_Steps.result o last_elem) tacis
    4.20      	val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
    4.21      	  (_, SOME (ist, ctxt)) => (ist, ctxt)
    4.22        | (_, NONE) => raise ERROR "Derive.embed Frm: uncovered case get_obj"
    4.23 +      val (res, asm) = ((State_Steps.result ctxt) o last_elem) tacis
    4.24      	val (f, _) = Ctree.get_obj Ctree.g_result pt p
    4.25      	val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
    4.26      	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::

     5.1 --- a/src/Tools/isac/Interpret/error-pattern.sml	Thu Jan 26 13:31:07 2023 +0100
     5.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml	Thu Jan 26 18:54:25 2023 +0100
     5.3 @@ -155,27 +155,31 @@
     5.4  *)
     5.5  fun filled_exactly (pt, pos as (p, _)) istr =
     5.6    (* input from Isabelle/PIDE: TODO handle Position *)
     5.7 -  case TermC.parseNEW (Ctree.get_ctxt pt pos) istr of
     5.8 -    NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
     5.9 -  | SOME ifo => 
    5.10 -      let
    5.11 -        val p' = Pos.lev_on p;
    5.12 -        val tac = Ctree.get_obj Ctree.g_tac pt p';
    5.13 -      in 
    5.14 -        case Solve_Step.check tac (pt, pos) of
    5.15 -          Applicable.No msg => (msg, Tactic.Tac "")
    5.16 -        | Applicable.Yes rew =>
    5.17 -            let
    5.18 -              val res = case rew of
    5.19 -               Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
    5.20 -              |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
    5.21 -              | t => raise ERROR ("filled_exactly: uncovered case for " ^ Tactic.string_of t)
    5.22 -            in 
    5.23 -              if not (ifo = res) then
    5.24 -                ("input does not exactly fill the gaps", Tactic.Tac "")
    5.25 -              else ("ok", tac)
    5.26 -            end
    5.27 -      end
    5.28 +  let
    5.29 +    val ctxt = Ctree.get_ctxt pt pos
    5.30 +  in
    5.31 +    case TermC.parseNEW (Ctree.get_ctxt pt pos) istr of
    5.32 +      NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
    5.33 +    | SOME ifo => 
    5.34 +        let
    5.35 +          val p' = Pos.lev_on p;
    5.36 +          val tac = Ctree.get_obj Ctree.g_tac pt p';
    5.37 +        in 
    5.38 +          case Solve_Step.check tac (pt, pos) of
    5.39 +            Applicable.No msg => (msg, Tactic.Tac "")
    5.40 +          | Applicable.Yes rew =>
    5.41 +              let
    5.42 +                val res = case rew of
    5.43 +                  Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
    5.44 +                | Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
    5.45 +                | t => raise ERROR ("filled_exactly: uncovered case for " ^ Tactic.string_of ctxt t)
    5.46 +              in 
    5.47 +                if not (ifo = res) then
    5.48 +                  ("input does not exactly fill the gaps", Tactic.Tac "")
    5.49 +                else ("ok", tac)
    5.50 +              end
    5.51 +        end
    5.52 +   end
    5.53  
    5.54  (* fetch errpatIDs from an arbitrary tactic *)
    5.55  fun from_store ctxt tac =

     6.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Thu Jan 26 13:31:07 2023 +0100
     6.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Thu Jan 26 18:54:25 2023 +0100
     6.3 @@ -126,7 +126,7 @@
     6.4  fun trace_msg_3 ctxt tac =
     6.5    if Config.get ctxt LI_trace then
     6.6      tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^
     6.7 -      "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"")
     6.8 +      "@@@ tac_ = \"" ^ Tactic.string_of ctxt tac ^ "\"")
     6.9    else ();
    6.10  fun associate _ ctxt (m as Tactic.Rewrite_Inst'
    6.11          (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =

     7.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Thu Jan 26 13:31:07 2023 +0100
     7.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Thu Jan 26 18:54:25 2023 +0100
     7.3 @@ -107,12 +107,12 @@
     7.4          let
     7.5            val m' = snd (Sub_Problem.tac_from_prog (pt, p) prog_tac)
     7.6          in
     7.7 -          Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'), ctxt)
     7.8 +          Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result ctxt m'), ctxt)
     7.9          end
    7.10      | _ =>
    7.11        (case Solve_Step.check m (pt, p) of
    7.12          Applicable.Yes m' => 
    7.13 -          Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'),
    7.14 +          Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result ctxt m'),
    7.15              Tactic.insert_assumptions m' ctxt)
    7.16        | _ => Reject_Tac)
    7.17    end
    7.18 @@ -322,7 +322,8 @@
    7.19           AssOnly => Term_Val1 act_arg
    7.20         | _(*ORundef*) =>
    7.21            case Solve_Step.check (LItool.tac_from_prog (pt, p) prog_tac) (pt, p) of
    7.22 -             Applicable.Yes m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
    7.23 +             Applicable.Yes m' =>
    7.24 +              Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result ctxt m'), ctxt, tac)
    7.25             | Applicable.No _ => Term_Val1 act_arg)
    7.26  
    7.27  (** scan to a Prog_Tac **)
    7.28 @@ -489,7 +490,7 @@
    7.29            if assoc then
    7.30              Safe_Step (Pstate ist, ctxt, tac')
    7.31   	        else Unsafe_Step (Pstate ist, ctxt, tac')
    7.32 -      | Reject_Tac1 _ => Not_Locatable (Tactic.string_of tac ^ " not locatable")
    7.33 +      | Reject_Tac1 _ => Not_Locatable (Tactic.string_of ctxt tac ^ " not locatable")
    7.34        | err => raise ERROR ("not-found-in-program: NotLocatable from " ^ @{make_string} err))
    7.35    | locate_input_tactic _ _ _ _ _ = raise ERROR "locate_input_tactic: uncovered case in definition"
    7.36  
    7.37 @@ -543,7 +544,7 @@
    7.38                   ("ok", ([(Tactic.Apply_Method mI, show, (pos, (ist', ctxt')))], c, (pt, pos)))
    7.39                  end
    7.40              | tac =>
    7.41 -                raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac)
    7.42 +              raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of ctxt' tac)
    7.43            end
    7.44        end
    7.45    | by_tactic (Tactic.Check_Postcond' (pI, _)) (sub_ist, sub_ctxt) (pt, pos as (p, _)) =

     8.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Thu Jan 26 13:31:07 2023 +0100
     8.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Thu Jan 26 18:54:25 2023 +0100
     8.3 @@ -386,8 +386,8 @@
     8.4        in
     8.5          ((p, Pos.Pbl), c, Test_Out.FormKF f, pt)
     8.6        end
     8.7 -  | add m' _ (_, pos) =
     8.8 -      raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
     8.9 +  | add m' (_, ctxt) (_, pos) =
    8.10 +      raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of ctxt m' ^ " at " ^ Pos.pos'2str pos)
    8.11  
    8.12  (* LI switches between solve-phase and specify-phase *)
    8.13  fun add_general tac ic cs =

     9.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Thu Jan 26 13:31:07 2023 +0100
     9.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Thu Jan 26 18:54:25 2023 +0100
     9.3 @@ -165,14 +165,14 @@
     9.4    list;
     9.5  
     9.6  \<^isac_test>\<open>
     9.7 -fun ets2s (l,(m,eno,env,iar,res,s)) = 
     9.8 -  "\n(" ^ TermC.string_of_path l ^ ",(" ^ Tactic.string_of m ^
     9.9 +fun ets2s ctxt (l,(m,eno,env,iar,res,s)) = 
    9.10 +  "\n(" ^ TermC.string_of_path l ^ ",(" ^ Tactic.string_of ctxt m ^
    9.11    ",\n  ens= " ^ Env.subst2str eno ^
    9.12    ",\n  env= " ^ Env.subst2str env ^
    9.13    ",\n  iar= " ^ UnparseC.term iar ^
    9.14    ",\n  res= " ^ UnparseC.term res ^
    9.15    ",\n  " ^ Celem.safe2str s ^ "))";
    9.16 -fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets;
    9.17 +fun ets2str ctxt (ets: ets) = (strs2str o (map (ets2s ctxt))) ets;
    9.18  \<close>
    9.19  
    9.20  type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)

    10.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml	Thu Jan 26 13:31:07 2023 +0100
    10.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml	Thu Jan 26 18:54:25 2023 +0100
    10.3 @@ -20,8 +20,8 @@
    10.4  
    10.5    type o_model
    10.6    type o_model_single
    10.7 -  val o_model_to_string : o_model -> string
    10.8 -  val o_model_single_to_string : o_model_single -> string
    10.9 +  val o_model_to_string : Proof.context ->  o_model -> string
   10.10 +  val o_model_single_to_string : Proof.context -> o_model_single -> string
   10.11    val o_model_empty : o_model_single
   10.12  
   10.13    type i_model
   10.14 @@ -68,10 +68,11 @@
   10.15  type o_model = o_model_single list;  
   10.16  val o_model_empty = (0, [], "", TermC.empty, [TermC.empty]) : o_model_single;
   10.17  
   10.18 -fun o_model_single_to_string (i, vs, fi, t, ts) = 
   10.19 +fun o_model_single_to_string ctxt (i, vs, fi, t, ts) = 
   10.20    "(" ^ string_of_int i ^ ", " ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
   10.21 -  UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
   10.22 -val o_model_to_string = strs2str' o (map (linefeed o o_model_single_to_string));
   10.23 +  UnparseC.term_in_ctxt ctxt t ^ ", " ^ (strs2str o (map (UnparseC.term_in_ctxt ctxt))) ts ^ ")";
   10.24 +fun o_model_to_string ctxt o_model =
   10.25 +  (strs2str' o (map (linefeed o (o_model_single_to_string ctxt)))) o_model;
   10.26  
   10.27  
   10.28  (** definitions for I_Model.T **)

    11.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Thu Jan 26 13:31:07 2023 +0100
    11.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Thu Jan 26 18:54:25 2023 +0100
    11.3 @@ -11,7 +11,7 @@
    11.4    val single_empty : single
    11.5    type T
    11.6    val to_string : Proof.context -> T -> string
    11.7 -  val result : single -> (term * term list)
    11.8 +  val result : Proof.context -> single -> (term * term list)
    11.9    val make_single: Proof.context -> Rewrite_Ord.id * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
   11.10      single
   11.11    val insert_pos : Pos.pos -> T -> T
   11.12 @@ -38,15 +38,15 @@
   11.13      (Istate_Def.T * Proof.context)))  (* after applying tac_, for ctree generation *)
   11.14  val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
   11.15  fun taci2str ctxt ((tac, tac_, (pos', (istate, _))): single) =
   11.16 -  "( " ^ Tactic.input_to_string ctxt tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
   11.17 +  "( " ^ Tactic.input_to_string ctxt tac ^ ", " ^ Tactic.string_of ctxt tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
   11.18    Istate_Def.string_of ctxt istate ^ " ))"
   11.19  
   11.20  type T = single list;
   11.21  
   11.22  fun to_string ctxt tacis = (strs2str o (map (linefeed o (taci2str ctxt)))) tacis
   11.23 -fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
   11.24 -  | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
   11.25 -  | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_)
   11.26 +fun result _ (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
   11.27 +  | result _ (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
   11.28 +  | result ctxt (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of ctxt tac_)
   11.29  
   11.30  fun make_single ctxt ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) = 
   11.31      (Tactic.Rewrite (id, thm), 

    12.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Thu Jan 26 13:31:07 2023 +0100
    12.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Thu Jan 26 18:54:25 2023 +0100
    12.3 @@ -41,7 +41,7 @@
    12.4    | Begin_Trans' of term | End_Trans' of Celem.result
    12.5    | End_Proof''
    12.6  
    12.7 -  val string_of: T -> string
    12.8 +  val string_of: Proof.context -> T -> string
    12.9  
   12.10    datatype input =
   12.11      Add_Find of TermC.as_string | Add_Given of TermC.as_string
   12.12 @@ -90,8 +90,8 @@
   12.13    val for_specify: input -> bool
   12.14  
   12.15    val input_from_T : Proof.context -> T -> input
   12.16 -  val result : T -> term
   12.17 -  val creates_assms: T -> term list
   12.18 +  val result : Proof.context -> T -> term
   12.19 +  val creates_assms: Proof.context -> T -> term list
   12.20    val insert_assumptions: T -> Proof.context -> Proof.context
   12.21    val for_specify': T -> bool
   12.22  end
   12.23 @@ -373,7 +373,7 @@
   12.24    | End_Trans' of Celem.result  (* for intermediate steps into Rewrite_Set   *)
   12.25    | End_Proof''
   12.26  
   12.27 -fun string_of ma = case ma of
   12.28 +fun string_of ctxt ma = case ma of
   12.29      Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
   12.30    | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
   12.31      strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
   12.32 @@ -389,11 +389,11 @@
   12.33    | Specify_Problem' (pI, (ok, _)) =>  "Specify_Problem' " ^ 
   12.34      spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str where_")))
   12.35    | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^ 
   12.36 -    MethodC.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )"
   12.37 +    MethodC.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string ctxt oris ^ ", )"
   12.38  
   12.39    | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
   12.40    | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
   12.41 -      (spair2str (strs2str pblID, UnparseC.term scval))
   12.42 +      (spair2str (strs2str pblID, UnparseC.term_in_ctxt ctxt scval))
   12.43  
   12.44    | Free_Solve' => "Free_Solve'"
   12.45  
   12.46 @@ -401,7 +401,8 @@
   12.47    | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
   12.48    | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
   12.49    | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ ", " ^ bool2str pasm ^
   12.50 -    ", " ^ Rule_Set.id rls' ^ ", " ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ ", " ^ UnparseC.terms asm ^ "))"
   12.51 +    ", " ^ Rule_Set.id rls' ^ ", " ^ UnparseC.term_in_ctxt ctxt f ^ ",(" ^
   12.52 +      UnparseC.term_in_ctxt ctxt f' ^ ", " ^ UnparseC.terms_in_ctxt ctxt asm ^ "))"
   12.53    | End_Detail' _ => "End_Detail' xxx"
   12.54  
   12.55    | Derive' rls => "Derive' " ^ Rule_Set.id rls
   12.56 @@ -449,24 +450,25 @@
   12.57    | input_from_T _ (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
   12.58    | input_from_T _ (Check_Postcond' (pblID, _)) = Check_Postcond pblID
   12.59    | input_from_T _ Empty_Tac_ = Empty_Tac
   12.60 -  | input_from_T _ m = raise ERROR (": not impl. for "^(string_of m));
   12.61 +  | input_from_T ctxt m = raise ERROR (": not impl. for " ^ string_of ctxt m);
   12.62  
   12.63 -fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
   12.64 -  | res (Rewrite' (_, _, _, _, _, _, res)) = res
   12.65 -  | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
   12.66 -  | res (Rewrite_Set' (_, _, _, _, res)) = res
   12.67 -  | res (Calculate' (_, _, _, (t, _))) = (t, [])
   12.68 -  | res (Check_elementwise' (_, _, res)) = res
   12.69 -  | res (Subproblem' (_, _, _, _, _, t)) = (t, [])
   12.70 -  | res (Take' t) = (t, [])
   12.71 -  | res (Substitute' (_, _, _, _, t)) = (t, [])
   12.72 -  | res (Or_to_List' (_,  t)) = (t, [])
   12.73 -  | res m = raise ERROR ("result: not impl.for " ^ string_of m)
   12.74 +fun res _ (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
   12.75 +  | res _ (Rewrite' (_, _, _, _, _, _, res)) = res
   12.76 +  | res _ (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
   12.77 +  | res _ (Rewrite_Set' (_, _, _, _, res)) = res
   12.78 +  | res _ (Calculate' (_, _, _, (t, _))) = (t, [])
   12.79 +  | res _ (Check_elementwise' (_, _, res)) = res
   12.80 +  | res _ (Subproblem' (_, _, _, _, _, t)) = (t, [])
   12.81 +  | res _ (Take' t) = (t, [])
   12.82 +  | res _ (Substitute' (_, _, _, _, t)) = (t, [])
   12.83 +  | res _ (Or_to_List' (_,  t)) = (t, [])
   12.84 +  | res ctxt m = raise ERROR ("result: not impl.for " ^ string_of ctxt m)
   12.85  
   12.86 -fun result tac = (fst o res) tac;
   12.87 -fun creates_assms tac = (snd o res) tac;
   12.88 +fun result ctxt tac = (fst o (res ctxt)) tac;
   12.89 +fun creates_assms ctxt tac = (snd o (res ctxt)) tac;
   12.90  
   12.91 -fun insert_assumptions tac ctxt  = ContextC.insert_assumptions (creates_assms tac) ctxt
   12.92 +(*fun insert_assumptions tac ctxt  = ContextC.insert_assumptions (creates_assms tac) ctxt*)
   12.93 +fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms ctxt tac) ctxt
   12.94  
   12.95  fun for_specify (Add_Find _) = true
   12.96    | for_specify (Add_Given _) = true

    13.1 --- a/src/Tools/isac/Specify/m-match.sml	Thu Jan 26 13:31:07 2023 +0100
    13.2 +++ b/src/Tools/isac/Specify/m-match.sml	Thu Jan 26 18:54:25 2023 +0100
    13.3 @@ -179,9 +179,10 @@
    13.4  (* match each pat of the model-pattern with an actual argument;
    13.5     precondition: copy-named vars are filtered out            *)
    13.6  fun matc _ [] _ oris = oris
    13.7 -  | matc _ pbt [] _ =
    13.8 +  | matc thy pbt [] _ =
    13.9      (tracing (dashs 70);
   13.10 -     raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
   13.11 +     raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string
   13.12 +       (Proof_Context.init_global thy) pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
   13.13    | matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
   13.14      (*del?..*)if (O_Model.is_copy_named' o TermC.free2str) t then oris
   13.15      else(*..del?*)
   13.16 @@ -213,9 +214,9 @@
   13.17      val pats = (#model o Problem.from_store ctxt) pI
   13.18      val msg = (dots 70 ^ "\n"
   13.19         ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
   13.20 -       ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
   13.21 -       ^ "*** stac   '" ^ UnparseC.term stac ^ "' has the ...\n"
   13.22 -       ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
   13.23 +       ^ "*** model-pattern " ^ Model_Pattern.to_string ctxt pats ^ "\n"
   13.24 +       ^ "*** stac   '" ^ UnparseC.term_in_ctxt ctxt stac ^ "' has the ...\n"
   13.25 +       ^ "*** arg-list " ^ UnparseC.terms_in_ctxt ctxt ags ^ "\n"
   13.26         ^ dashs 70)
   13.27    in tracing msg end
   13.28  

    14.1 --- a/src/Tools/isac/Specify/o-model.sml	Thu Jan 26 13:31:07 2023 +0100
    14.2 +++ b/src/Tools/isac/Specify/o-model.sml	Thu Jan 26 18:54:25 2023 +0100
    14.3 @@ -27,8 +27,8 @@
    14.4    type descriptor
    14.5    type values
    14.6    type message
    14.7 -  val to_string: T -> string
    14.8 -  val single_to_string: single -> string
    14.9 +  val to_string: Proof.context -> T -> string
   14.10 +  val single_to_string: Proof.context -> single -> string
   14.11    val single_empty: single
   14.12  
   14.13    val init: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context
   14.14 @@ -83,6 +83,7 @@
   14.15  val empty = [] : Model_Def.o_model;
   14.16  type single = Model_Def.o_model_single
   14.17  val single_empty = Model_Def.o_model_empty;
   14.18 +
   14.19  val single_to_string = Model_Def.o_model_single_to_string;
   14.20  val to_string = Model_Def.o_model_to_string;
   14.21  

    15.1 --- a/src/Tools/isac/Specify/specify-step.sml	Thu Jan 26 13:31:07 2023 +0100
    15.2 +++ b/src/Tools/isac/Specify/specify-step.sml	Thu Jan 26 18:54:25 2023 +0100
    15.3 @@ -183,7 +183,7 @@
    15.4        in
    15.5          ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
    15.6        end
    15.7 -  | add m' _ (_, pos) =
    15.8 -      raise ERROR ("Specify_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
    15.9 +  | add m' (_, ctxt) (_, pos) =
   15.10 +      raise ERROR ("Specify_Step.add: not impl.for " ^ Tactic.string_of ctxt m' ^ " at " ^ Pos.pos'2str pos)
   15.11  
   15.12  (**)end(**);

    16.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Thu Jan 26 13:31:07 2023 +0100
    16.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Thu Jan 26 18:54:25 2023 +0100
    16.3 @@ -464,10 +464,10 @@
    16.4       val Applicable.Yes m' =
    16.5            (*case*) Solve_Step.check (LItool.tac_from_prog (pt, p) prog_tac) (pt, p) (*of*);
    16.6  
    16.7 -  Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
    16.8 +  Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result @{context} m'), ctxt, tac)
    16.9            (*return from check_tac1*);
   16.10  "~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1  \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
   16.11 -  (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
   16.12 +  (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result @{context} m'), ctxt, tac));
   16.13  
   16.14  val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
   16.15  val ([3], Res) = p;

    17.1 --- a/test/Tools/isac/Knowledge/diff-app.sml	Thu Jan 26 13:31:07 2023 +0100
    17.2 +++ b/test/Tools/isac/Knowledge/diff-app.sml	Thu Jan 26 18:54:25 2023 +0100
    17.3 @@ -311,7 +311,7 @@
    17.4  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    17.5  === inhibit exn 110722=============================================================*)
    17.6  
    17.7 -val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
    17.8 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string @{context} oris);
    17.9  val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
   17.10  
   17.11  (*=== inhibit exn 110722=============================================================
   17.12 @@ -380,7 +380,7 @@
   17.13  val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e; 
   17.14  === inhibit exn 110722=============================================================*)
   17.15  
   17.16 -val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string oris);
   17.17 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(O_Model.to_string @{context} oris);
   17.18  
   17.19  val pits = get_obj g_pbl pt (fst p);writeln(I_Model.to_string ctxt pits);
   17.20  val pits = get_obj g_pbl pt [];writeln(I_Model.to_string ctxt pits);

    18.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml	Thu Jan 26 13:31:07 2023 +0100
    18.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml	Thu Jan 26 18:54:25 2023 +0100
    18.3 @@ -22,8 +22,8 @@
    18.4  Rewrite': ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T;
    18.5  val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
    18.6  ;
    18.7 -if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";
    18.8 -if (Tactic.creates_assms tac |> UnparseC.terms) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";
    18.9 +if (Tactic.result ctxt tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";
   18.10 +if (Tactic.creates_assms ctxt tac |> UnparseC.terms) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED";
   18.11  
   18.12  
   18.13  "----------- fun subst_adapt_to_type -----------------------------------------------------------";

    19.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Thu Jan 26 13:31:07 2023 +0100
    19.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Thu Jan 26 18:54:25 2023 +0100
    19.3 @@ -154,7 +154,7 @@
    19.4  		     val (c', ptp) =
    19.5      Derive.embed tacis' ptp;
    19.6  "~~~~~ fun embed , args:"; val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);
    19.7 -      val (res, asm) = (State_Steps.result o last_elem) tacis
    19.8 +      val (res, asm) = ((State_Steps.result ctxt) o last_elem) tacis
    19.9      	val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
   19.10      	  (_, SOME (ist, ctxt)) => (ist, ctxt)
   19.11        | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"

    20.1 --- a/test/Tools/isac/Specify/i-model.sml	Thu Jan 26 13:31:07 2023 +0100
    20.2 +++ b/test/Tools/isac/Specify/i-model.sml	Thu Jan 26 18:54:25 2023 +0100
    20.3 @@ -51,13 +51,13 @@
    20.4          val cmI = if mI = MethodC.id_empty then mI' else mI
    20.5          val {model, where_, where_rls, ...} = Problem.from_store ctxt cpI;
    20.6  
    20.7 -(*+*)if Model_Pattern.to_string model = "[\"" ^
    20.8 +(*+*)if Model_Pattern.to_string @{context} model = "[\"" ^
    20.9    "(#Given, (Traegerlaenge, l_l))\", \"" ^
   20.10    "(#Given, (Streckenlast, q_q))\", \"" ^
   20.11    "(#Find, (Biegelinie, b_b))\", \"" ^
   20.12    "(#Relate, (Randbedingungen, r_b))\"]"
   20.13  (*+*)then () else error "INITIAL Model_Pattern CHANGED";
   20.14 -(*+*)if O_Model.to_string oris = "[\n" ^
   20.15 +(*+*)if O_Model.to_string @{context} oris = "[\n" ^
   20.16    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
   20.17    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
   20.18    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
   20.19 @@ -83,7 +83,7 @@
   20.20  (**)val ("", ori', all) =(**)
   20.21            (*case*) O_Model.contains ctxt m_field o_model t (*of*);
   20.22  
   20.23 -(*+*)O_Model.single_to_string ori';
   20.24 +(*+*)O_Model.single_to_string @{context} ori';
   20.25  (*+*)val [Free ("q_0", _)] = all;
   20.26  
   20.27  (** )val ("", (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)])))) =( **)

    21.1 --- a/test/Tools/isac/Specify/o-model.sml	Thu Jan 26 13:31:07 2023 +0100
    21.2 +++ b/test/Tools/isac/Specify/o-model.sml	Thu Jan 26 18:54:25 2023 +0100
    21.3 @@ -99,7 +99,7 @@
    21.4  "~~~~~ from fun O_Model.init \<longrightarrow>fun initialise' , return:"; val (pors, pctxt) = (oris, ctxt);
    21.5  
    21.6  (* final test ...*)
    21.7 -(*+*)if O_Model.to_string pors = "[\n" ^ 
    21.8 +(*+*)if O_Model.to_string @{context} pors = "[\n" ^ 
    21.9    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^ 
   21.10    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^ 
   21.11    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^ 

    22.1 --- a/test/Tools/isac/Specify/specify.sml	Thu Jan 26 13:31:07 2023 +0100
    22.2 +++ b/test/Tools/isac/Specify/specify.sml	Thu Jan 26 18:54:25 2023 +0100
    22.3 @@ -100,8 +100,8 @@
    22.4  (*** Problem model is complete ============================================================ ***)
    22.5   val ctxt = ThyC.id_to_ctxt "Diff_App";
    22.6   val (o_model, _, _) = get_obj g_origin pt (fst p);
    22.7 - writeln (O_Model.to_string o_model);
    22.8 -if O_Model.to_string o_model = "[\n" ^
    22.9 + writeln (O_Model.to_string @{context} o_model);
   22.10 +if O_Model.to_string @{context} o_model = "[\n" ^
   22.11    "(1, [\"1\", \"2\", \"3\"], #Given, fixedValues, [\"[r = Arbfix]\"]), \n" ^
   22.12    "(2, [\"1\", \"2\", \"3\"], #Find, maximum, [\"A\"]), \n" ^
   22.13    "(3, [\"1\", \"2\", \"3\"], #Find, valuesFor, [\"[a]\", \"[b]\"]), \n" ^
   22.14 @@ -212,7 +212,7 @@
   22.15  val "(7 ,[1] ,true ,#undef ,Cor FunctionVariable a ,(funvar, [a]))" = I_Model.single_to_string @{context} xxx;
   22.16  (*-------------------- stop step into do_all -------------------------------------------------*)
   22.17  (*/------------------- check result of I_Model.complete' ------------------------------------\*)
   22.18 -if Model_Pattern.to_string_PIDE @{context} mod_pat = "[\"" ^
   22.19 +if Model_Pattern.to_string @{context} mod_pat = "[\"" ^
   22.20    "(#Given, (Constants, fixes))\", \"" ^
   22.21    "(#Given, (Maximum, maxx))\", \"" ^
   22.22    "(#Given, (Extremum, extr))\", \"" ^
   22.23 @@ -275,7 +275,7 @@
   22.24  (*/------------------- check result of Test_Code.init_calc @{context} ----------------------------------------\*)
   22.25  (*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =
   22.26    get_obj g_origin pt (fst p);
   22.27 -(*+*)if O_Model.to_string o_model = "[\n" ^
   22.28 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
   22.29    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
   22.30    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
   22.31    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
   22.32 @@ -306,7 +306,7 @@
   22.33    Calc.specify_data (pt, p);
   22.34  (*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])
   22.35  (*+*)then () else error "initial o_refs CHANGED";
   22.36 -(*+*)if O_Model.to_string o_model = "[\n" ^
   22.37 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
   22.38    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
   22.39    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
   22.40    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
   22.41 @@ -334,7 +334,7 @@
   22.42  (*/------------------- check for entry to Step.by_tactic -----------------------------------\*)
   22.43  (*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;
   22.44  (*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);
   22.45 -(*+*)if O_Model.to_string o_model = "[\n" ^
   22.46 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
   22.47    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
   22.48    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
   22.49    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
   22.50 @@ -367,7 +367,7 @@
   22.51  
   22.52     O_Model.complete_for m_patt root_model (o_model, ctxt);
   22.53  (*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)
   22.54 -(*+*)Model_Pattern.to_string m_patt = "[\"" ^
   22.55 +(*+*)Model_Pattern.to_string @{context}  m_patt = "[\"" ^
   22.56    "(#Given, (Traegerlaenge, l))\", \"" ^
   22.57    "(#Given, (Streckenlast, q))\", \"" ^
   22.58    "(#Given, (FunktionsVariable, v))\", \"" ^
   22.59 @@ -375,7 +375,7 @@
   22.60    "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
   22.61    "(#Find, (Biegelinie, b))\", \"" ^
   22.62    "(#Relate, (Randbedingungen, s))\"]";
   22.63 -(*+*) O_Model.to_string root_model = "[\n" ^ (*.. = o_model for Pos.([], _) *)
   22.64 +(*+*) O_Model.to_string @{context} root_model = "[\n" ^ (*.. = o_model for Pos.([], _) *)
   22.65    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
   22.66    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
   22.67    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
   22.68 @@ -406,7 +406,7 @@
   22.69      ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));
   22.70  
   22.71  (*/------------------- check of result from O_Model.complete_for -----------------------------------\*)
   22.72 -(*+*)if O_Model.to_string o_model' = "[\n" ^
   22.73 +(*+*)if O_Model.to_string @{context} o_model' = "[\n" ^
   22.74    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
   22.75    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
   22.76    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
   22.77 @@ -447,7 +447,7 @@
   22.78  
   22.79  (*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)
   22.80  (*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);
   22.81 -(*+*)O_Model.to_string o_model = "[\n" ^
   22.82 +(*+*)O_Model.to_string @{context} o_model = "[\n" ^
   22.83    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
   22.84    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
   22.85    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
   22.86 @@ -488,7 +488,7 @@
   22.87        Step.specify_do_next (pt, input_pos);
   22.88  (*/------------------- check result of specify_do_next -------------------------------------\*)
   22.89  (*+*)val {origin = (ooo_mod, _, _), meth, ...} =  Calc.specify_data (pt'''''_'', p'''''_'');
   22.90 -(*+*)if O_Model.to_string ooo_mod = "[\n" ^
   22.91 +(*+*)if O_Model.to_string @{context} ooo_mod = "[\n" ^
   22.92    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
   22.93    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
   22.94    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
   22.95 @@ -525,7 +525,7 @@
   22.96      val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
   22.97  "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
   22.98  (*/------------------- check within find_next_step -----------------------------------------\*)
   22.99 -(*+*)Model_Pattern.to_string (MethodC.from_store ctxt mI' |> #model) = "[\"" ^
  22.100 +(*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^
  22.101    "(#Given, (Traegerlaenge, l))\", \"" ^
  22.102    "(#Given, (Streckenlast, q))\", \"" ^
  22.103    "(#Given, (FunktionsVariable, v))\", \"" ^   (* <---------- take m_field from here !!!*)
  22.104 @@ -560,7 +560,7 @@
  22.105    "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
  22.106    "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
  22.107  (*+*)then () else error "icl within item_to_add CHANGED";
  22.108 -(*+*)if O_Model.to_string vors = "[\n" ^
  22.109 +(*+*)if O_Model.to_string @{context} vors = "[\n" ^
  22.110    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
  22.111    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.112    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
  22.113 @@ -646,7 +646,7 @@
  22.114  (*+*)m_field = "#Given";
  22.115  (*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;
  22.116  (*+*)val [Free ("x", _)] = vals;
  22.117 -(*+*)O_Model.to_string ori = "[\n" ^
  22.118 +(*+*)O_Model.to_string @{context} ori = "[\n" ^
  22.119    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
  22.120    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.121    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
  22.122 @@ -670,7 +670,7 @@
  22.123  (*+*)val ([1], Pbl) = p;
  22.124  (*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
  22.125    get_obj g_origin pt (fst p);
  22.126 -(*+*)if O_Model.to_string o_model = "[\n" ^
  22.127 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
  22.128    "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.129    "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
  22.130    "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
  22.131 @@ -707,7 +707,7 @@
  22.132  (*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)
  22.133  (*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
  22.134    get_obj g_origin pt (fst p);
  22.135 -(*+*)if O_Model.to_string o_model = "[\n" ^                                         
  22.136 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^                                         
  22.137    "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.138    "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
  22.139    "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
  22.140 @@ -730,19 +730,19 @@
  22.141  (*/------------------- check for entry to O_Model.complete_for -----------------------------\*)
  22.142  (*+*)if mID = ["Biegelinien", "ausBelastung"]
  22.143  (*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";
  22.144 -(*+*)if Model_Pattern.to_string m_patt = "[\"" ^
  22.145 +(*+*)if Model_Pattern.to_string @{context} m_patt = "[\"" ^
  22.146    "(#Given, (Streckenlast, q__q))\", \"" ^
  22.147    "(#Given, (FunktionsVariable, v_v))\", \"" ^
  22.148    "(#Given, (Biegelinie, id_fun))\", \"" ^          (*.. add value from O_Model of root-problem*)
  22.149    "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^ (*.. add value from O_Model of root-problem*)
  22.150    "(#Find, (Funktionen, fun_s))\"]"
  22.151  (*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";
  22.152 -(*+*)if O_Model.to_string o_model = "[\n" ^
  22.153 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
  22.154    "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.155    "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
  22.156    "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]" 
  22.157  (*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";
  22.158 -(*+*)if O_Model.to_string root_model = "[\n" ^
  22.159 +(*+*)if O_Model.to_string @{context} root_model = "[\n" ^
  22.160    "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
  22.161    "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.162    "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
  22.163 @@ -751,7 +751,7 @@
  22.164    "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
  22.165    "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
  22.166  (*+*)then () else error "[Biegelinien, ausBelastung] root O_Model CHANGED";
  22.167 -(*+*)if O_Model.to_string o_model' = "[\n" ^   (*.. OK: is value of O_Model.complete_for *)
  22.168 +(*+*)if O_Model.to_string @{context} o_model' = "[\n" ^   (*.. OK: is value of O_Model.complete_for *)
  22.169    "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.170    "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
  22.171    "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
  22.172 @@ -788,7 +788,7 @@
  22.173      ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
  22.174  
  22.175  (*/------------------- check within O_Model.complete_for -------------------------------------------\*)
  22.176 -(*+*)if O_Model.to_string o_model' = "[\n" ^   (*.. OK: is return from step into *)
  22.177 +(*+*)if O_Model.to_string @{context} o_model' = "[\n" ^   (*.. OK: is return from step into *)
  22.178    "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.179    "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
  22.180    "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
  22.181 @@ -844,7 +844,7 @@
  22.182        spec = refs, ...} = Calc.specify_data (pt, pos);
  22.183      val ctxt = Ctree.get_ctxt pt pos
  22.184  ;
  22.185 -(*+*)O_Model.to_string oris = "[\n" ^
  22.186 +(*+*)O_Model.to_string @{context} oris = "[\n" ^
  22.187    "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.188    "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
  22.189    "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
  22.190 @@ -895,7 +895,7 @@
  22.191     check_single ctxt m_field oris i_model m_patt ct (*of*);
  22.192  
  22.193  (*/------------------- check for entry to check_single -------------------------------------\*)
  22.194 -(*+*)if O_Model.to_string oris = "[\n" ^
  22.195 +(*+*)if O_Model.to_string @{context} oris = "[\n" ^
  22.196    "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
  22.197    "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
  22.198    "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
  22.199 @@ -933,7 +933,7 @@
  22.200  "~~~~~ ~~~ fun associate_input' , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
  22.201  
  22.202  (*+/---------------- bypass recursion of associate_input' ----------------\*)
  22.203 -(*+*)O_Model.to_string oris = "[\n" ^
  22.204 +(*+*)O_Model.to_string @{context} oris = "[\n" ^
  22.205    "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
  22.206    "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
  22.207    "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
  22.208 @@ -948,20 +948,20 @@
  22.209  (*+*)then () else error "associate_input' Model_Pattern CHANGED";
  22.210  (*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)
  22.211  (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
  22.212 -(*+*)if (Problem.from_store ctxt ["vonBelastungZu", "Biegelinien"] |> #model |> Model_Pattern.to_string) = "[\"" ^
  22.213 +(*+*)if (Problem.from_store ctxt ["vonBelastungZu", "Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
  22.214    "(#Given, (Streckenlast, q_q))\", \"" ^
  22.215    "(#Given, (FunktionsVariable, v_v))\", \"" ^
  22.216    "(#Find, (Funktionen, funs'''))\"]"
  22.217  (*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";
  22.218  (* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up> *)
  22.219 -(*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #model |> Model_Pattern.to_string) = "[\"" ^
  22.220 +(*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
  22.221    "(#Given, (Traegerlaenge, l_l))\", \"" ^
  22.222    "(#Given, (Streckenlast, q_q))\", \"" ^
  22.223    "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)
  22.224    "(#Relate, (Randbedingungen, r_b))\"]"
  22.225  (*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";
  22.226  (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
  22.227 -(*+*)if (MethodC.from_store ctxt ["Biegelinien", "ausBelastung"] |> #model |> Model_Pattern.to_string) = "[\"" ^
  22.228 +(*+*)if (MethodC.from_store ctxt ["Biegelinien", "ausBelastung"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
  22.229    "(#Given, (Streckenlast, q__q))\", \"" ^
  22.230    "(#Given, (FunktionsVariable, v_v))\", \"" ^
  22.231    "(#Given, (Biegelinie, id_fun))\", \"" ^ (*--------------------------------- \<up> *)