1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Sat Feb 04 11:21:56 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy	Sat Feb 04 16:20:45 2023 +0100
     1.3 @@ -63,16 +63,6 @@
     1.4  
     1.5  ML \<open>
     1.6  \<close> ML \<open>
     1.7 -fun T_from_program t = (t 
     1.8 -  |> HOLogic.dest_list 
     1.9 -  |> map HOLogic.dest_prod 
    1.10 -  |> map (apfst HOLogic.dest_string))
    1.11 -  |> map (apfst (fn e1 => (TermC.mk_Free (e1, HOLogic.realT))))
    1.12 -  handle TERM _ => raise TERM ("T_from_program: wrong argument ", [t])
    1.13 -\<close> ML \<open>
    1.14 -\<close> ML \<open>
    1.15 -\<close> ML \<open>
    1.16 -\<close> ML \<open>
    1.17  \<close> ML \<open>
    1.18  \<close>
    1.19  end

     2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sat Feb 04 11:21:56 2023 +0100
     2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Sat Feb 04 16:20:45 2023 +0100
     2.3 @@ -88,7 +88,7 @@
     2.4    val set_ref_last_thy: theory -> unit
     2.5    val get_via_last_thy: ThyC.id -> theory (*only used for * (Sub-)problem retrieving respective thy
     2.6                                                            * problem refinement                    
     2.7 -                                                          * (test-)code to be deleted            *)
     2.8 +                                                          * in fun UnparseC.term_ERROR           *)
     2.9  end;
    2.10  
    2.11  structure Know_Store(**): KNOW_STORE(**) =

     3.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Sat Feb 04 11:21:56 2023 +0100
     3.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Sat Feb 04 16:20:45 2023 +0100
     3.3 @@ -11,6 +11,8 @@
     3.4    val empty: term
     3.5    val typ_empty: typ
     3.6  
     3.7 +  val unparse_ERROR: term -> as_string
     3.8 +
     3.9    datatype lrd = D | L | R
    3.10    type path
    3.11    val string_of_path: path -> string
    3.12 @@ -119,6 +121,18 @@
    3.13  val empty = UnparseC.term_empty
    3.14  val typ_empty = UnparseC.typ_empty
    3.15  
    3.16 +(*
    3.17 +  functions in abstraction far off context sometimes raise an ERROR at a respective term;
    3.18 +  in order not to spoil the signature of these functions,
    3.19 +  the context for unparsing the term is taken by Know_Store.get_via_last_thy.
    3.20 +*)
    3.21 +fun unparse_ERROR t =
    3.22 +  let
    3.23 +    val ctxt = "Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global
    3.24 +  in
    3.25 +    UnparseC.term_in_ctxt ctxt t
    3.26 +  end
    3.27 +
    3.28  datatype lrd = L (*t1 in "t1$t2"*)
    3.29               | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*)
    3.30  type path = lrd list; 
    3.31 @@ -133,7 +147,7 @@
    3.32    | sub_at (R :: p) (_ $ t2) = sub_at p t2
    3.33    | sub_at l t = raise TERM ("sub_at: no " ^ string_of_path l ^ " for ", [t]);
    3.34  fun go_up l t =
    3.35 -  if length l > 1 then sub_at (drop_last l) t else raise ERROR ("go_up [] " ^ UnparseC.term t)
    3.36 +  if length l > 1 then sub_at (drop_last l) t else raise ERROR ("go_up [] " ^ unparse_ERROR t)
    3.37  
    3.38  fun isastr_of_int i = if i >= 0 then string_of_int i else "-" ^ string_of_int (abs i)
    3.39  
    3.40 @@ -241,11 +255,10 @@
    3.41  
    3.42  fun string_of_num n = (n |> HOLogic.dest_number |> snd |> string_of_int)
    3.43  
    3.44 -(* refer to Thm.lhs_of *)
    3.45  fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
    3.46 -  | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
    3.47 +  | lhs t = raise TERM ("lhs called with ", [t]);
    3.48  fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
    3.49 -  | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");
    3.50 +  | rhs t = raise TERM ("rhs called with ", [t]);
    3.51  
    3.52  
    3.53  fun mk_negative T t = Const (\<^const_name>\<open>uminus\<close>, T --> T) $ t
    3.54 @@ -341,7 +354,7 @@
    3.55  fun guess_bdv_typ t = t |> vars |> hd |> type_of
    3.56  
    3.57  fun free2str (Free (s, _)) = s
    3.58 -  | free2str t = raise ERROR ("free2str not for " ^ UnparseC.term t);
    3.59 +  | free2str t = raise TERM ("free2str not for ", [t]);
    3.60  fun str_of_free_opt (Free (s, _)) = SOME s
    3.61    | str_of_free_opt _ = NONE
    3.62  
    3.63 @@ -371,7 +384,7 @@
    3.64  
    3.65  fun isapair2pair (Const (\<^const_name>\<open>Pair\<close>,_) $ a $ b) = (a, b)
    3.66    | isapair2pair t = 
    3.67 -    raise ERROR ("isapair2pair called with " ^ UnparseC.term t);
    3.68 +    raise TERM ("isapair2pair called with ", [t]);
    3.69  fun isalist2list ls =
    3.70    let
    3.71      fun get es (Const(\<^const_name>\<open>Cons\<close>, _) $ t $ ls) = get (t :: es) ls
    3.72 @@ -596,5 +609,4 @@
    3.73  	    | SOME cs => ins_concl cs (mk_equality (rhs, lhs))
    3.74    in trm' end
    3.75  
    3.76 -
    3.77  end

     4.1 --- a/src/Tools/isac/BaseDefinitions/unparseC.sml	Sat Feb 04 11:21:56 2023 +0100
     4.2 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml	Sat Feb 04 16:20:45 2023 +0100
     4.3 @@ -11,7 +11,8 @@
     4.4    val typ_empty: typ
     4.5  
     4.6    val term_in_ctxt: Proof.context -> term -> term_as_string
     4.7 -  val term: term -> term_as_string
     4.8 +  val term: term -> term_as_string (*remains until final replace "_in_ctxt" \<longrightarrow> "" *)
     4.9 +(*val term_ERROR \<longrightarrow> TermC.unparse_ERROR: term -> term_as_string, due to file dependencies*)
    4.10  
    4.11    val term_in_thy: theory -> term -> term_as_string
    4.12    val term_opt: Proof.context -> term option -> term_as_string
    4.13 @@ -41,7 +42,6 @@
    4.14    end;
    4.15  fun terms_in_ctxt ctxt ts = ts |> map (term_in_ctxt ctxt) |> strs2str';
    4.16  
    4.17 -
    4.18  fun term t = term_in_ctxt (ThyC.id_to_ctxt "Isac_Knowledge") t;
    4.19  fun term_in_thy thy t = term_in_ctxt (Proof_Context.init_global thy) t;
    4.20  fun terms_in_thy thy ts = ts |> map (term_in_thy thy) |> strs2str';

     5.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Sat Feb 04 11:21:56 2023 +0100
     5.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml	Sat Feb 04 16:20:45 2023 +0100
     5.3 @@ -177,7 +177,7 @@
     5.4    XML.Elem (("THEOREM", []), [
     5.5      XML.Elem (("ID", []), [XML.Text ID]),
     5.6      XML.Elem (("FORMULA", []), [
     5.7 -      XML.Text ((UnparseC.term o Thm.prop_of) thm)])])           (* repair for MathML: use term instead String *)
     5.8 +      XML.Text ((TermC.unparse_ERROR o Thm.prop_of) thm)])]) (* repair for MathML: use term instead String *)
     5.9  
    5.10  fun xml_of_src Rule.Empty_Prog =
    5.11      XML.Elem (("NOCODE", []), [XML.Text "empty"])

     6.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml	Sat Feb 04 11:21:56 2023 +0100
     6.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml	Sat Feb 04 16:20:45 2023 +0100
     6.3 @@ -65,7 +65,7 @@
     6.4  (*WN071016 checked that _all_ Frontend/interface.sml uses this*)
     6.5  fun term2xml j t = 
     6.6      indt (j+i) ^ "<MATHML>\n" ^ 
     6.7 -    indt (j+2*i) ^ "<ISA> " ^ (decode o UnparseC.term) t ^ " </ISA>\n" ^
     6.8 +    indt (j+2*i) ^ "<ISA> " ^ (decode o TermC.unparse_ERROR) t ^ " </ISA>\n" ^
     6.9      indt (j+i) ^ "</MATHML>";
    6.10  (*val t = TermC.parse_test @{context} "equality e_";
    6.11    writeln (term2xml 8 t);
    6.12 @@ -74,13 +74,13 @@
    6.13            <MATHML> *)
    6.14  fun xml_of_term t =
    6.15    XML.Elem (("MATHML", []),
    6.16 -    [XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)])])
    6.17 +    [XML.Elem (("ISA", []), [XML.Text ((decode o TermC.unparse_ERROR) t)])])
    6.18  fun xml_of_terms ts = map xml_of_term ts
    6.19  
    6.20  (* intermediate replacements while introducing transfer of terms by libisabelle *)
    6.21  fun xml_of_term_NEW (t : term) =
    6.22    XML.Elem (("FORMULA", []), [
    6.23 -    XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)]),
    6.24 +    XML.Elem (("ISA", []), [XML.Text ((decode o TermC.unparse_ERROR) t)]),
    6.25      XML.Text ("(TERM)\n " ^ UnparseC.term t  ^ "\n(/TERM)")
    6.26      ])
    6.27  

     7.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sat Feb 04 11:21:56 2023 +0100
     7.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Sat Feb 04 16:20:45 2023 +0100
     7.3 @@ -22,7 +22,7 @@
     7.4    val check_leaf: string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term -> 
     7.5        Program.leaf * term option
     7.6  
     7.7 -  val implicit_take: Program.T -> Env.T -> term option
     7.8 +  val implicit_take: Proof.context -> Program.T -> Env.T -> term option
     7.9    val get_simplifier: Calc.T -> Rule_Set.T
    7.10    val tac_from_prog: Ctree.state -> term -> Tactic.input
    7.11  (*from isac_test for Minisubpbl*)
    7.12 @@ -44,9 +44,9 @@
    7.13  open Pos
    7.14  
    7.15  (* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
    7.16 -fun implicit_take (Rule.Prog prog) env =
    7.17 +fun implicit_take ctxt (Rule.Prog prog) env =
    7.18      Option.map (subst_atomic env) (Prog_Tac.get_first_argument prog)
    7.19 -  | implicit_take _ _ = raise ERROR "implicit_take: no match";
    7.20 +  | implicit_take _ _ _ = raise ERROR "implicit_take: no match";
    7.21  
    7.22  (*  *)
    7.23  val error_msg_1 = "ERROR: the guard is missing (#model in 'type met' added in prep_met)."

     8.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Sat Feb 04 11:21:56 2023 +0100
     8.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Sat Feb 04 16:20:45 2023 +0100
     8.3 @@ -510,7 +510,7 @@
     8.4           val (is, env, ctxt, prog) = case LItool.init_pstate prog_rls ctxt itms mI of
     8.5             (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
     8.6           | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
     8.7 -        val ini = LItool.implicit_take prog env;
     8.8 +        val ini = LItool.implicit_take ctxt prog env;
     8.9          val pos = start_new_level pos
    8.10        in 
    8.11          case ini of

     9.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Sat Feb 04 11:21:56 2023 +0100
     9.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Sat Feb 04 16:20:45 2023 +0100
     9.3 @@ -82,7 +82,7 @@
     9.4          | scan t = case Prog_Tac.eval_leaf [] NONE TermC.empty t of
     9.5    			  (Program.Tac _, _) => [t] | (Program.Expr _, _) => []
     9.6      in ((distinct op =) o scan) body end
     9.7 -  | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ UnparseC.term t ^ "'")
     9.8 +  | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ TermC.unparse_ERROR t ^ "'")
     9.9  
    9.10  (* get operators out of a program *)
    9.11  fun is_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _) = true
    9.12 @@ -90,7 +90,7 @@
    9.13    | is_calc _ = false;
    9.14  fun op_of_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op_) = HOLogic.dest_string op_
    9.15    | op_of_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op_ $ _) = HOLogic.dest_string op_
    9.16 -  | op_of_calc t = raise ERROR ("op_of_calc called with " ^ UnparseC.term t);
    9.17 +  | op_of_calc t = raise ERROR ("op_of_calc called with " ^ TermC.unparse_ERROR t);
    9.18  fun get_calcs thy sc =
    9.19      sc
    9.20      |> stacpbls

    10.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Sat Feb 04 11:21:56 2023 +0100
    10.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Sat Feb 04 16:20:45 2023 +0100
    10.3 @@ -60,7 +60,7 @@
    10.4  signature PROGAM_TACTIC =
    10.5  sig
    10.6    val dest_spec : term -> References_Def.T
    10.7 -  val get_first_argument : term -> term option (*TODO rename get_first_argument*)
    10.8 +  val get_first_argument : term -> term option
    10.9    val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
   10.10    val is: term -> bool
   10.11  
   10.12 @@ -121,7 +121,8 @@
   10.13  
   10.14        | get_t _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
   10.15      in get_t body TermC.empty end
   10.16 -  | get_first_argument t = raise ERROR ("get_first_argument: no fun-def. for " ^ UnparseC.term t);
   10.17 +  | get_first_argument t =
   10.18 +    raise ERROR ("get_first_argument: no fun-def. for " ^ TermC.unparse_ERROR t);
   10.19  
   10.20  (* substitute the Istate.T's environment to a leaf of the program
   10.21     and attach the curried argument of a tactic, if any.

    11.1 --- a/src/Tools/isac/ProgLang/Program.thy	Sat Feb 04 11:21:56 2023 +0100
    11.2 +++ b/src/Tools/isac/ProgLang/Program.thy	Sat Feb 04 16:20:45 2023 +0100
    11.3 @@ -60,7 +60,7 @@
    11.4  datatype leaf = Tac of term | Expr of term
    11.5  fun rep_stacexpr (Tac t ) = t
    11.6    | rep_stacexpr (Expr t) = 
    11.7 -    raise ERROR ("rep_stacexpr called with t= " ^ UnparseC.term t);
    11.8 +    raise ERROR ("rep_stacexpr called with t= " ^ TermC.unparse_ERROR t);
    11.9  
   11.10  (* the lucas-interpreter LI requires programs in this specific format *)
   11.11  fun prep_program thm = (thm

    12.1 --- a/src/Tools/isac/ProgLang/evaluate.sml	Sat Feb 04 11:21:56 2023 +0100
    12.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml	Sat Feb 04 16:20:45 2023 +0100
    12.3 @@ -23,7 +23,7 @@
    12.4    val adhoc_thm: Proof.context -> Eval_Def.ml -> term -> (string * thm) option
    12.5    val adhoc_thm1_: Proof.context -> Eval_Def.ml -> term -> (string * thm) option
    12.6    val norm: term -> term
    12.7 -  val popt2str: ('a * term) option -> string
    12.8 +  val popt2str: Proof.context -> ('a * term) option -> string
    12.9    val int_of_numeral: term -> int
   12.10  \<^isac_test>\<open>
   12.11    val get_pair: Proof.context -> string -> Eval_Def.ml_fun -> term -> (string * term) option
   12.12 @@ -95,8 +95,8 @@
   12.13  
   12.14  (** calculate numerals **)
   12.15  
   12.16 -fun popt2str (SOME (_, term)) = "SOME " ^ UnparseC.term term (*TODO \<longrightarrow> str_of_termopt*)
   12.17 -  | popt2str NONE = "NONE";
   12.18 +fun popt2str ctxt (SOME (_, term)) = "SOME " ^ UnparseC.term_in_ctxt ctxt term (*TODO \<longrightarrow> str_of_termopt*)
   12.19 +  | popt2str _ NONE = "NONE";
   12.20  
   12.21  (* scan a term for applying eval_fn ef 
   12.22  args
   12.23 @@ -115,11 +115,13 @@
   12.24  fun trace_calc1 ctxt str1 str2 =
   12.25    if Config.get ctxt eval_trace then writeln (str1 ^ str2) else ()
   12.26  fun trace_calc2 ctxt str term popt =
   12.27 -  if Config.get ctxt eval_trace then writeln (str ^ UnparseC.term_in_ctxt ctxt term ^ " , " ^ popt2str popt) else ()
   12.28 +  if Config.get ctxt eval_trace
   12.29 +  then writeln (str ^ UnparseC.term_in_ctxt ctxt term ^ " , " ^ popt2str ctxt popt) else ()
   12.30  fun trace_calc3 ctxt str term =
   12.31    if Config.get ctxt eval_trace then writeln ("### " ^ str ^ UnparseC.term_in_ctxt ctxt term) else ()
   12.32  fun trace_calc4 ctxt str t1 t2 =
   12.33 -  if Config.get ctxt eval_trace then writeln ("### " ^ str ^ UnparseC.term_in_ctxt ctxt t1 ^ " $ " ^ UnparseC.term_in_ctxt ctxt t2) else ()
   12.34 +  if Config.get ctxt eval_trace
   12.35 +  then writeln ("### " ^ str ^ UnparseC.term_in_ctxt ctxt t1 ^ " $ " ^ UnparseC.term_in_ctxt ctxt t2) else ()
   12.36  
   12.37  fun get_pair (*1*)ctxt  op_ (ef: ml_fun) (t as (Const (op0, _) $ arg)) =   (* unary fns *)
   12.38      if op_ = op0 then 

    13.1 --- a/src/Tools/isac/Specify/Input_Descript.thy	Sat Feb 04 11:21:56 2023 +0100
    13.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy	Sat Feb 04 16:20:45 2023 +0100
    13.3 @@ -199,7 +199,7 @@
    13.4    | join (d, ts) = 
    13.5      case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
    13.6        SOME x => x
    13.7 -    | NONE => raise ERROR ("join: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 
    13.8 +    | NONE => raise ERROR ("join: " ^ TermC.unparse_ERROR d ^ " $ " ^ TermC.unparse_ERROR (hd ts)); 
    13.9  fun join' (d, []) = 
   13.10      if for_real_list d
   13.11      then (d $ e_listReal)
   13.12 @@ -207,7 +207,7 @@
   13.13    | join' (d, ts) = 
   13.14      case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
   13.15        SOME x => x
   13.16 -    | NONE => raise ERROR ("join': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 
   13.17 +    | NONE => raise ERROR ("join': " ^ TermC.unparse_ERROR d ^ " $ " ^ TermC.unparse_ERROR (hd ts)); 
   13.18  fun join''' (d, []) = 
   13.19      if for_real_list d
   13.20      then UnparseC.term (d $ e_listReal)
   13.21 @@ -217,7 +217,7 @@
   13.22    | join''' (d, ts) = 
   13.23      case \<^try>\<open> UnparseC.term (d $ (join'''' (d, ts)))\<close> of
   13.24        SOME x => x
   13.25 -    | NONE => raise ERROR ("join''': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 
   13.26 +    | NONE => raise ERROR ("join''': " ^ TermC.unparse_ERROR d ^ " $ " ^ TermC.unparse_ERROR (hd ts)); 
   13.27  
   13.28  (**)end(**)
   13.29  \<close> ML \<open>

    14.1 --- a/src/Tools/isac/Specify/i-model.sml	Sat Feb 04 11:21:56 2023 +0100
    14.2 +++ b/src/Tools/isac/Specify/i-model.sml	Sat Feb 04 16:20:45 2023 +0100
    14.3 @@ -127,7 +127,7 @@
    14.4  (* get the constant value from a penv *)
    14.5  fun getval (id, values) = 
    14.6    case values of
    14.7 -	  [] => raise ERROR ("penv_value: no values in '" ^ UnparseC.term id)
    14.8 +	  [] => raise ERROR ("penv_value: no values in '" ^ TermC.unparse_ERROR id)
    14.9    | [v] => (id, v)
   14.10    | (v1 :: v2 :: _) => (case v1 of 
   14.11  	      Const (\<^const_name>\<open>Program.Arbfix\<close>, _) => (id, v2)
   14.12 @@ -371,9 +371,9 @@
   14.13  fun to_p_model _ (Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
   14.14    | to_p_model _ (Syn c) = c
   14.15    | to_p_model _ (Typ c) = c
   14.16 -  | to_p_model _ (Inc ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
   14.17 -  | to_p_model _ (Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))
   14.18 -  | to_p_model _ (Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
   14.19 +  | to_p_model thy (Inc ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
   14.20 +  | to_p_model thy (Sup (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
   14.21 +  | to_p_model thy (Mis (d, pid)) = UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term pid
   14.22    | to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"
   14.23  
   14.24  fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (descriptor itm_ = descriptor iitm_)

    15.1 --- a/src/Tools/isac/Specify/o-model.sml	Sat Feb 04 11:21:56 2023 +0100
    15.2 +++ b/src/Tools/isac/Specify/o-model.sml	Sat Feb 04 16:20:45 2023 +0100
    15.3 @@ -92,7 +92,7 @@
    15.4  \<^isac_test>\<open>
    15.5  fun preori2str (vs, fi, t, ts) = 
    15.6    "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
    15.7 -  UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
    15.8 +  UnparseC.term t ^ ", " ^ (strs2str o (map TermC.unparse_ERROR)) ts ^ ")";
    15.9  val string_of_preoris = (strs2str' o (map (linefeed o preori2str)));
   15.10  \<close>
   15.11  
   15.12 @@ -104,12 +104,12 @@
   15.13  (** initialise O_Model **)
   15.14  
   15.15  (* compare d and dsc in pbt and transfer field to where_-ori *)
   15.16 -fun add_field (_: theory) pbt (d,ts) = 
   15.17 +fun add_field thy pbt (d,ts) = 
   15.18    let fun eq d pt = (d = (fst o snd) pt);
   15.19    in case filter (eq d) pbt of
   15.20         [(fi, (_, _))] => (fi, d, ts)
   15.21       | [] => ("#undef", d, ts)   (*may come with met.model*)
   15.22 -     | _ => raise ERROR ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
   15.23 +     | _ => raise ERROR ("add_field: " ^ UnparseC.term_in_thy thy d ^ " more than once in pbt")
   15.24    end;
   15.25  
   15.26  (*
   15.27 @@ -266,7 +266,7 @@
   15.28      else ([1], field, dsc, [t])
   15.29  	\<close> of
   15.30      SOME x => x
   15.31 -  | NONE => raise ERROR ("copy_name: for "^ UnparseC.term t)
   15.32 +  | NONE => raise ERROR ("copy_name: for " ^ TermC.unparse_ERROR t)
   15.33  
   15.34  
   15.35  (** tools for I_Model **)

    16.1 --- a/src/Tools/isac/Specify/p-spec.sml	Sat Feb 04 11:21:56 2023 +0100
    16.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Sat Feb 04 16:20:45 2023 +0100
    16.3 @@ -29,7 +29,7 @@
    16.4    val imodel2fstr: iitem list -> (string * TermC.as_string) list
    16.5    val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
    16.6    val is_e_ts: term list -> bool
    16.7 -  val itms2fstr: I_Model.single -> string * string
    16.8 +  val itms2fstr: Proof.context -> I_Model.single -> string * string
    16.9    val par2fstr: I_Model.single -> string * TermC.as_string
   16.10    val parsitm: theory -> I_Model.single -> I_Model.single
   16.11    val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
   16.12 @@ -70,52 +70,52 @@
   16.13  val empty = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
   16.14  
   16.15  (* re-parse itms with a new thy and prepare for checking with ori list *)
   16.16 -fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
   16.17 +fun parsitm thy (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
   16.18      (case \<^try>\<open>
   16.19          let val t = Input_Descript.join (d, ts)
   16.20 -          val _ = (UnparseC.term_in_thy dI t)
   16.21 +          val _ = (UnparseC.term_in_thy thy t)
   16.22            (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
   16.23          in itm end\<close> of
   16.24        SOME x => x
   16.25      | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
   16.26 -  | parsitm dI (i, v, b, f, I_Model.Syn str) =
   16.27 +  | parsitm _ (i, v, b, f, I_Model.Syn str) =
   16.28      (case \<^try>\<open>
   16.29          let val _ = Syntax.read_term\<^context> str
   16.30          in (i, v, b ,f, I_Model.Par str) end\<close> of
   16.31        SOME x => x
   16.32      | NONE => (i, v, b, f, I_Model.Syn str))
   16.33 -  | parsitm dI (i, v, b, f, I_Model.Typ str) =
   16.34 +  | parsitm _ (i, v, b, f, I_Model.Typ str) =
   16.35      (case \<^try>\<open>
   16.36          let val _ = Syntax.read_term\<^context> str
   16.37           in (i, v, b, f, I_Model.Par str) end\<close> of
   16.38        SOME x => x
   16.39      | NONE => (i, v, b, f, I_Model.Syn str))
   16.40 -  | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
   16.41 +  | parsitm thy (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
   16.42      (case \<^try>\<open>
   16.43          let val t = Input_Descript.join (d,ts);
   16.44 -	        val _ = UnparseC.term_in_thy dI t;
   16.45 +	        val _ = UnparseC.term_in_thy thy t;
   16.46          (*this    ^ should raise the exn on unability of re-parsing dts*)
   16.47          in itm end\<close> of
   16.48        SOME x => x
   16.49      | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
   16.50 -  | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
   16.51 +  | parsitm thy (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
   16.52      (case \<^try>\<open>
   16.53          let val t = Input_Descript.join (d,ts);
   16.54 -	        val _ = UnparseC.term_in_thy dI t;
   16.55 +	        val _ = UnparseC.term_in_thy thy t;
   16.56          (*this    ^ should raise the exn on unability of re-parsing dts*)
   16.57          in itm end\<close> of
   16.58        SOME x => x
   16.59      | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
   16.60 -  | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
   16.61 +  | parsitm thy (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
   16.62      (case \<^try>\<open>
   16.63          let val t = d $ t';
   16.64 -	        val _ = UnparseC.term_in_thy dI t;
   16.65 +	        val _ = UnparseC.term_in_thy thy t;
   16.66          (*this    ^ should raise the exn on unability of re-parsing dts*)
   16.67          in itm end\<close> of
   16.68        SOME x => x
   16.69      | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
   16.70 -  | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) = 
   16.71 -    raise ERROR ("parsitm (" ^ I_Model.single_to_string (Proof_Context.init_global dI) itm ^
   16.72 +  | parsitm thy (itm as (_, _, _, _, I_Model.Par _)) = 
   16.73 +    raise ERROR ("parsitm (" ^ I_Model.single_to_string (Proof_Context.init_global thy) itm ^
   16.74        "): Par should be internal");
   16.75  
   16.76  (*separate a list to a pair of elements that do NOT satisfy the predicate,
   16.77 @@ -199,14 +199,14 @@
   16.78  
   16.79  fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
   16.80    | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
   16.81 -fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
   16.82 -  | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)
   16.83 -  | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)
   16.84 -  | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
   16.85 -  | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
   16.86 -  | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
   16.87 -  | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) = 
   16.88 -    raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
   16.89 +fun itms2fstr _ (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
   16.90 +  | itms2fstr _ (_, _, _, f, I_Model.Syn str) = (f, str)
   16.91 +  | itms2fstr _ (_, _, _, f, I_Model.Typ str) = (f, str)
   16.92 +  | itms2fstr _ (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
   16.93 +  | itms2fstr _ (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
   16.94 +  | itms2fstr ctxt (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term_in_ctxt ctxt (d $ t))
   16.95 +  | itms2fstr ctxt (itm as (_, _, _, _, I_Model.Par _)) = 
   16.96 +    raise ERROR ("parsitm (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");
   16.97  
   16.98  fun imodel2fstr iitems = 
   16.99    let 
  16.100 @@ -221,57 +221,57 @@
  16.101      let
  16.102  		  val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
  16.103  		    Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 
  16.104 -		      spec = sspec as (sdI, spI, smI), probl, meth, ...}
  16.105 +		      spec = sspec as (sdI, spI, smI), probl, meth, ctxt, ...}
  16.106          => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
  16.107        | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
  16.108        val thy = Know_Store.get_via_last_thy dI
  16.109 -(** ) val ctxt = Proof_Context.init_global (ThyC.get_theory sdI)( **)
  16.110 +      val ctxt = Proof_Context.init_global thy
  16.111      in if CAS_Cmd.is_from hdf fmz
  16.112 -       then the (CAS_Cmd.input (ParseC.term_opt (Proof_Context.init_global thy) hdf |> the)) 
  16.113 +       then the (CAS_Cmd.input (ParseC.term_opt ctxt hdf |> the)) 
  16.114         else
  16.115           let val (pos_, pits, mits) = 
  16.116  	         if dI <> sdI
  16.117  	         then let val its = map (parsitm (ThyC.get_theory dI)) probl;
  16.118  			            val (its, trms) = filter_sep is_Par its;
  16.119 -			            val pbt = (#model o Problem.from_store (Proof_Context.init_global thy))
  16.120 +			            val pbt = (#model o Problem.from_store ctxt)
  16.121  			              (#2 (References.select_input ospec sspec))
  16.122  		            in (Pos.Pbl, appl_adds dI oris its pbt  (map par2fstr trms), meth) end 
  16.123             else
  16.124               if pI <> spI 
  16.125  	           then if pI = snd3 ospec then (Pos.Pbl, probl, meth) 
  16.126                    else
  16.127 -		                let val pbt = (#model o Problem.from_store (Proof_Context.init_global thy)) pI
  16.128 +		                let val pbt = (#model o Problem.from_store ctxt) pI
  16.129  			                val dI' = #1 (References.select_input ospec spec)
  16.130  			                val oris =
  16.131  			                  if pI = #2 ospec then oris 
  16.132  				                else O_Model.init thy fmz_ pbt |> #1;
  16.133  		                in (Pos.Pbl, appl_adds dI' oris probl pbt 
  16.134 -				              (map itms2fstr probl), meth) end 
  16.135 +				              (map (itms2fstr ctxt) probl), meth) end 
  16.136               else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
  16.137 -	                then let val met = (#model o MethodC.from_store (Proof_Context.init_global thy)) mI
  16.138 +	                then let val met = (#model o MethodC.from_store ctxt) mI
  16.139  		                     val mits = I_Model.complete oris probl meth met
  16.140  		                   in if foldl and_ (true, map #3 mits)
  16.141  		                      then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) 
  16.142  		                   end 
  16.143                    else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
  16.144 -			                  ((#model o Problem.from_store (Proof_Context.init_global thy))
  16.145 +			                  ((#model o Problem.from_store ctxt)
  16.146  			                    (#2 (References.select_input ospec spec)))
  16.147  			                      (imodel2fstr imodel), meth)
  16.148  	         val pt = Ctree.update_spec pt p spec;
  16.149           in if pos_ = Pos.Pbl
  16.150  	          then 
  16.151  	            let 
  16.152 -	              val {where_rls, where_,...} = Problem.from_store (Proof_Context.init_global thy) 
  16.153 +	              val {where_rls, where_,...} = Problem.from_store ctxt
  16.154  	                (#2 (References.select_input ospec spec))
  16.155 -		            val (_, where_) = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ pits 0
  16.156 +		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ pits 0
  16.157  	            in (Ctree.update_pbl pt p pits,
  16.158  		                 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec)) 
  16.159                end
  16.160  	          else 
  16.161  	            let 
  16.162 -	              val {where_rls,where_,...} = MethodC.from_store (Proof_Context.init_global thy) 
  16.163 +	              val {where_rls,where_,...} = MethodC.from_store ctxt 
  16.164  	                (#3 (References.select_input ospec spec))
  16.165 -		            val (_, where_) = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ mits 0
  16.166 +		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
  16.167  	            in (Ctree.update_met pt p mits,
  16.168  		                  (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
  16.169                end

    17.1 --- a/src/Tools/isac/Specify/pre-conditions.sml	Sat Feb 04 11:21:56 2023 +0100
    17.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml	Sat Feb 04 16:20:45 2023 +0100
    17.3 @@ -8,7 +8,7 @@
    17.4    type T
    17.5    type unchecked
    17.6    type input
    17.7 -  val to_string : T -> string
    17.8 +  val to_string : Proof.context -> T -> string
    17.9  
   17.10    val check: Proof.context -> Rule_Set.T -> unchecked -> I_Model.T -> 'a -> bool * (bool * term) list
   17.11    val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
   17.12 @@ -23,13 +23,13 @@
   17.13  struct
   17.14  (**)
   17.15  
   17.16 +type T = Pre_Conds_Def.T;  (*= (bool * term) list;*)
   17.17  (*type checked = Pre_Conds_Def.T;*)
   17.18 -type T = Pre_Conds_Def.T;  (*= (bool * term) list;*)
   17.19  type unchecked = term list
   17.20  type input = TermC.as_string list;
   17.21  
   17.22 -fun to_str (b, t) = pair2str (bool2str b, UnparseC.term t);
   17.23 -fun to_string pres = strs2str' (map (linefeed o to_str) pres);
   17.24 +fun to_str ctxt (b, t) = pair2str (bool2str b, UnparseC.term_in_ctxt ctxt t);
   17.25 +fun to_string ctxt pres = strs2str' (map (linefeed o (to_str ctxt)) pres);
   17.26  
   17.27  fun eval _ _ (false, where_) = (false, where_) (*NOT ALL Free's have been substituted*)
   17.28    | eval ctxt where_rls (true, where_) =

    18.1 --- a/src/Tools/isac/Specify/sub-problem.sml	Sat Feb 04 11:21:56 2023 +0100
    18.2 +++ b/src/Tools/isac/Specify/sub-problem.sml	Sat Feb 04 16:20:45 2023 +0100
    18.3 @@ -47,6 +47,7 @@
    18.4      in
    18.5        (Tactic.Subproblem (dI, pI),	Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
    18.6      end
    18.7 -  | tac_from_prog _ t = raise ERROR ("Sub_Problem.tac_from_prog not impl. for " ^ UnparseC.term t)
    18.8 +  | tac_from_prog _ t =
    18.9 +    raise ERROR ("Sub_Problem.tac_from_prog not impl. for " ^ TermC.unparse_ERROR t)
   18.10  
   18.11  (**)end(**)

    19.1 --- a/test/Tools/isac/Interpret/li-tool.sml	Sat Feb 04 11:21:56 2023 +0100
    19.2 +++ b/test/Tools/isac/Interpret/li-tool.sml	Sat Feb 04 16:20:45 2023 +0100
    19.3 @@ -47,7 +47,7 @@
    19.4  val thy = ThyC.get_theory thy';
    19.5  val prog_rls = LItool.get_simplifier (pt, pos)
    19.6  val (is as Pstate {env, ...}, ctxt, sc) = init_pstate prog_rls ctxt itms mI;
    19.7 -val ini = implicit_take sc env;
    19.8 +val ini = implicit_take @{context} sc env;
    19.9  "----- fun implicit_take, args:"; val (Prog sc) = sc;
   19.10  "----- fun get_first_argument, args:"; val (y, h $ body) = (thy, sc);
   19.11  case get_first_argument sc of SOME (Free ("e_e", _)) => ()

    20.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Sat Feb 04 11:21:56 2023 +0100
    20.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Sat Feb 04 16:20:45 2023 +0100
    20.3 @@ -75,7 +75,7 @@
    20.4           val (is, env, ctxt, prog) = case LItool.init_pstate prog_rls ctxt itms mI of
    20.5             (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
    20.6           | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
    20.7 -        val ini = LItool.implicit_take prog env;
    20.8 +        val ini = LItool.implicit_take ctxt prog env;
    20.9          val pos = start_new_level pos
   20.10  val NONE =
   20.11          (*case*) ini (*of*);
   20.12 @@ -173,7 +173,7 @@
   20.13          (is as Istate.Pstate {env, ...}, ctxt, sc) =>  (is, env, ctxt, sc)
   20.14        | _ => error "solve Apply_Method: uncovered case init_pstate";
   20.15  (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
   20.16 -      val ini = LItool.implicit_take sc env;
   20.17 +      val ini = LItool.implicit_take ctxt sc env;
   20.18        val p = lev_dn p;
   20.19  
   20.20        val NONE = (*case*) ini (*of*);

    21.1 --- a/test/Tools/isac/Knowledge/eqsystem-1a.sml	Sat Feb 04 11:21:56 2023 +0100
    21.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1a.sml	Sat Feb 04 16:20:45 2023 +0100
    21.3 @@ -135,7 +135,7 @@
    21.4  (*+*)val "Pstate ([\"\n(e_s, [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2])\", \"\n(v_s, [c, c_2])\"], [], srls_normalise_2x2, NONE, \n??.empty, ORundef, false, true)" =
    21.5  (*+isa==isa2*)is |> Istate.string_of ctxt
    21.6  
    21.7 -        val ini = LItool.implicit_take prog env;
    21.8 +        val ini = LItool.implicit_take ctxt prog env;
    21.9          val pos = start_new_level pos
   21.10  val NONE =
   21.11          (*case*) ini (*of*);

    22.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Sat Feb 04 11:21:56 2023 +0100
    22.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Sat Feb 04 16:20:45 2023 +0100
    22.3 @@ -71,7 +71,7 @@
    22.4           val (is, env, ctxt, prog) = case LItool.init_pstate prog_rls ctxt itms mI of
    22.5             (is as Istate.Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
    22.6           | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
    22.7 -        val ini = LItool.implicit_take prog env;
    22.8 +        val ini = LItool.implicit_take ctxt prog env;
    22.9          val pos = start_new_level pos
   22.10          val SOME t = (*case*) ini (*of*);
   22.11              val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);

    23.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Sat Feb 04 11:21:56 2023 +0100
    23.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Sat Feb 04 16:20:45 2023 +0100
    23.3 @@ -80,7 +80,7 @@
    23.4  (*+*)(ContextC.get_assumptions ctxt |> map (UnparseC.term_in_ctxt ctxt))
    23.5  (*+isa==isa2*)  = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"]; 
    23.6  
    23.7 -        val ini = LItool.implicit_take prog env;
    23.8 +        val ini = LItool.implicit_take ctxt prog env;
    23.9          val pos = start_new_level pos
   23.10  val SOME t =
   23.11        (*case*) ini (*of*);

    24.1 --- a/test/Tools/isac/Specify/refine.sml	Sat Feb 04 11:21:56 2023 +0100
    24.2 +++ b/test/Tools/isac/Specify/refine.sml	Sat Feb 04 16:20:45 2023 +0100
    24.3 @@ -423,7 +423,7 @@
    24.4          item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
    24.5        (*if*) not preok (*then*);
    24.6  
    24.7 -(*+*)Pre_Conds.to_string xxxxx = "[\n" ^
    24.8 +(*+*)Pre_Conds.to_string @{context} xxxxx = "[\n" ^
    24.9    "(false, matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^
   24.10      "matches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^
   24.11      "matches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^