1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Tue Jan 10 10:01:05 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Tue Jan 10 17:07:53 2023 +0100
     1.3 @@ -184,7 +184,7 @@
     1.4  
     1.5  fun id_from_rule _ (Rule.Rls_ rls) = id rls
     1.6    | id_from_rule ctxt r =
     1.7 -    raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string_PIDE ctxt r);
     1.8 +    raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string ctxt r);
     1.9  
    1.10  (* check if a rule is contained in a rule-set (recursivley down in Rls_);
    1.11     this rule can even be a rule-set itself                             *)

     2.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml	Tue Jan 10 10:01:05 2023 +0100
     2.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml	Tue Jan 10 17:07:53 2023 +0100
     2.3 @@ -14,17 +14,16 @@
     2.4    val set_id: Rule_Def.rule_set -> string
     2.5    val id: rule -> string
     2.6    val equal: rule * rule -> bool
     2.7 -  val to_string: rule -> string
     2.8 -  val to_string_PIDE: Proof.context -> rule -> string
     2.9 +  val to_string: Proof.context -> rule -> string
    2.10    val to_string_short: rule -> string
    2.11    val s_to_string: rule list -> string
    2.12  
    2.13 -  val thm: rule -> thm
    2.14 +  val thm: Proof.context -> rule -> thm
    2.15    val distinct' : rule list -> rule list
    2.16  
    2.17    val thm_id: rule -> string
    2.18 -  val eval: rule -> string * Rule_Def.eval_fn
    2.19 -  val rls: rule -> Rule_Def.rule_set
    2.20 +  val eval: Proof.context -> rule -> string * Rule_Def.eval_fn
    2.21 +  val rls: Proof.context -> rule -> Rule_Def.rule_set
    2.22  
    2.23    val make_eval: string -> Rule_Def.eval_fn -> rule
    2.24  end
    2.25 @@ -58,17 +57,12 @@
    2.26    | equal _ = false;
    2.27  fun distinct' rs = distinct equal rs
    2.28  
    2.29 -fun to_string_PIDE _ Rule_Def.Erule = "Erule" 
    2.30 -  | to_string_PIDE ctxt (Rule_Def.Thm (str, thm)) =
    2.31 +fun to_string _ Rule_Def.Erule = "Erule" 
    2.32 +  | to_string ctxt (Rule_Def.Thm (str, thm)) =
    2.33      "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm_PIDE ctxt thm ^ ")"
    2.34 -  | to_string_PIDE _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
    2.35 -  | to_string_PIDE _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
    2.36 -  | to_string_PIDE _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
    2.37 -fun to_string Rule_Def.Erule = "Erule" 
    2.38 -  | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm thm ^ ")"
    2.39 -  | to_string (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
    2.40 -  | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
    2.41 -  | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
    2.42 +  | to_string _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
    2.43 +  | to_string _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
    2.44 +  | to_string _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
    2.45  fun to_string_short Rule_Def.Erule = "Erule"
    2.46    | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
    2.47    | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
    2.48 @@ -78,13 +72,13 @@
    2.49  
    2.50  fun thm_id (Rule_Def.Thm (id, _)) = id
    2.51    | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *))
    2.52 -fun thm (Rule_Def.Thm (_, thm)) = thm
    2.53 -  | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r)
    2.54 +fun thm _ (Rule_Def.Thm (_, thm)) = thm
    2.55 +  | thm ctxt r = raise ERROR ("Rule.thm: uncovered case " ^ to_string ctxt r)
    2.56  
    2.57 -fun eval (Eval e) = e
    2.58 -  | eval r = raise ERROR ("Rule.eval NOT FOR " ^ to_string r)
    2.59 -fun rls (Rls_ rls) = rls
    2.60 -  | rls r = raise ERROR ("Rule.rls NOT FOR " ^ to_string r) 
    2.61 +fun eval _ (Eval e) = e
    2.62 +  | eval ctxt r = raise ERROR ("Rule.eval NOT FOR " ^ to_string ctxt r)
    2.63 +fun rls _ (Rls_ rls) = rls
    2.64 +  | rls ctxt r = raise ERROR ("Rule.rls NOT FOR " ^ to_string ctxt r) 
    2.65  
    2.66  
    2.67  (* ML antiquotations *)

     3.1 --- a/src/Tools/isac/Interpret/derive.sml	Tue Jan 10 10:01:05 2023 +0100
     3.2 +++ b/src/Tools/isac/Interpret/derive.sml	Tue Jan 10 17:07:53 2023 +0100
     3.3 @@ -100,7 +100,7 @@
     3.4            (case Rewrite.rewrite_set_ ctxt true rls t of
     3.5              NONE => rew_once lim rts t apno rs'
     3.6            | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
     3.7 -        | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string_PIDE ctxt rule))
     3.8 +        | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string ctxt rule))
     3.9      | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"
    3.10    in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end
    3.11  

     4.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Tue Jan 10 10:01:05 2023 +0100
     4.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Jan 10 17:07:53 2023 +0100
     4.3 @@ -491,7 +491,9 @@
     4.4  fun locate_rule thy eval_rls ro [rs] t r =
     4.5      if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
     4.6      then 
     4.7 -      let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t;
     4.8 +      let
     4.9 +        val ctxt = Proof_Context.init_global thy
    4.10 +        val ropt = Rewrite.rewrite_ ctxt ro eval_rls true (Rule.thm ctxt r) t;
    4.11        in
    4.12          case ropt of SOME ta => [(r, ta)]
    4.13  	      | NONE => ((*tracing 
    4.14 @@ -552,7 +554,9 @@
    4.15  fun locate_rule thy eval_rls ro [rs] t r =
    4.16      if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
    4.17      then 
    4.18 -      let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t;
    4.19 +      let
    4.20 +        val ctxt = Proof_Context.init_global thy
    4.21 +        val ropt = Rewrite.rewrite_ ctxt ro eval_rls true (Rule.thm ctxt r) t;
    4.22        in 
    4.23          case ropt of
    4.24            SOME ta => [(r, ta)]

     5.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml	Tue Jan 10 10:01:05 2023 +0100
     5.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml	Tue Jan 10 17:07:53 2023 +0100
     5.3 @@ -86,14 +86,14 @@
     5.4  val empty = Pstate e_pstate;
     5.5  
     5.6  fun rta2str ctxt (r, (t, a)) =
     5.7 -  "\n(" ^ Rule.to_string_PIDE ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^
     5.8 +  "\n(" ^ Rule.to_string ctxt r ^ ", (" ^ UnparseC.term_in_ctxt ctxt t ^ ", " ^
     5.9    UnparseC.terms_in_ctxt ctxt a ^ "))";
    5.10  fun string_of _ Uistate = "Uistate"
    5.11    | string_of _ (Pstate pst) = 
    5.12      "Pstate " ^ pstate2str pst   
    5.13    | string_of ctxt (RrlsState (t, t1, rss, rtas)) =
    5.14      "RrlsState (" ^ UnparseC.term t ^ ", " ^ UnparseC.term_in_ctxt ctxt t1 ^ ", " ^
    5.15 -    (strs2str o (map (strs2str o (map (Rule.to_string_PIDE ctxt))))) rss ^ ", " ^
    5.16 +    (strs2str o (map (strs2str o (map (Rule.to_string ctxt))))) rss ^ ", " ^
    5.17      (strs2str o (map (rta2str ctxt))) rtas ^ ")";
    5.18  fun string_of' Uistate = "Uistate"
    5.19    | string_of' (Pstate pst) = 

     6.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Jan 10 10:01:05 2023 +0100
     6.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Jan 10 17:07:53 2023 +0100
     6.3 @@ -207,7 +207,7 @@
     6.4              (case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of
     6.5                SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
     6.6              | NONE => rew_once ruls asm ct apno thms)
     6.7 -          | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string_PIDE ctxt r ^ "\"");
     6.8 +          | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string ctxt r ^ "\"");
     6.9        val ruls = (#rules o Rule_Set.rep) rls;
    6.10        val _ = trace_eq1 ctxt i "rls" rls ct
    6.11        val (ct', asm') = rew_once ruls [] ct Noap ruls;

     7.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Tue Jan 10 10:01:05 2023 +0100
     7.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Tue Jan 10 17:07:53 2023 +0100
     7.3 @@ -57,7 +57,7 @@
     7.4        Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
     7.5       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
     7.6    | make_single ctxt _ _ (t, r, _) = raise ERROR ("State_Steps.make_single: not impl. for " ^
     7.7 -    Rule.to_string_PIDE ctxt r ^ " at " ^ UnparseC.term_in_ctxt ctxt t)
     7.8 +    Rule.to_string ctxt r ^ " at " ^ UnparseC.term_in_ctxt ctxt t)
     7.9  
    7.10  (* update pos in tacis for embedding by generate *)
    7.11  fun insert_pos (_: Pos.pos) [] = []

     8.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Tue Jan 10 10:01:05 2023 +0100
     8.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Tue Jan 10 17:07:53 2023 +0100
     8.3 @@ -260,7 +260,7 @@
     8.4    | rule2tac ctxt subst (Rule.Rls_ rls) = 
     8.5      Rewrite_Set_Inst (Subst.T_to_input ctxt subst, (Rule_Set.id rls))
     8.6    | rule2tac ctxt _ rule = 
     8.7 -    raise ERROR ("rule2tac: called with \"" ^ Rule.to_string_PIDE ctxt rule ^ "\"");
     8.8 +    raise ERROR ("rule2tac: called with \"" ^ Rule.to_string ctxt rule ^ "\"");
     8.9  
    8.10  (* try if a rewrite-rule is applicable to a given formula; 
    8.11     in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 

     9.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Tue Jan 10 10:01:05 2023 +0100
     9.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Tue Jan 10 17:07:53 2023 +0100
     9.3 @@ -65,7 +65,7 @@
     9.4  fun of_thm thm = (id_of_thm thm, thm);
     9.5  fun from_rule _ (Rule.Thm (id, thm)) = (id, thm)
     9.6    | from_rule ctxt r =
     9.7 -    raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string_PIDE ctxt r);
     9.8 +    raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string ctxt r);
     9.9  
    9.10  \<^isac_test>\<open>
    9.11  fun string_of_thm_in_thy thy thm =
    9.12 @@ -151,7 +151,7 @@
    9.13          | _ => "sym_" ^ thmID
    9.14        in Rule.Thm (thmID', thm') end
    9.15    | make_sym_rule _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
    9.16 -  | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^  Rule.to_string_PIDE ctxt r)
    9.17 +  | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^  Rule.to_string ctxt r)
    9.18  
    9.19  \<^isac_test>\<open>
    9.20  (* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *)
    9.21 @@ -167,7 +167,7 @@
    9.22        else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*)
    9.23    | revert_sym_rule thy rule =
    9.24      raise ERROR ("ThmC.revert_sym_rule: NOT for " ^
    9.25 -      Rule.to_string_PIDE (Proof_Context.init_global thy) rule)
    9.26 +      Rule.to_string (Proof_Context.init_global thy) rule)
    9.27  \<close>
    9.28  
    9.29  

    10.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Tue Jan 10 10:01:05 2023 +0100
    10.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Tue Jan 10 17:07:53 2023 +0100
    10.3 @@ -132,7 +132,8 @@
    10.4    | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string 
    10.5      (get_calc_prog_id (Proof_Context.init_global thy) c)))
    10.6    | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.id rls))
    10.7 -  | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.to_string r ^ "\"");
    10.8 +  | rule2stac thy r = raise ERROR ("rule2stac: not applicable to \"" ^
    10.9 +      Rule.to_string (Proof_Context.init_global thy) r ^ "\"");
   10.10  fun rule2stac_inst _ (Rule.Thm (thmID, _)) = 
   10.11      Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID))
   10.12    | rule2stac_inst thy (Rule.Eval (c, _)) = 
   10.13 @@ -141,7 +142,8 @@
   10.14      Try $ (Repeat $ (Cal $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c)))
   10.15    | rule2stac_inst _ (Rule.Rls_ rls) = 
   10.16      Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.id rls))
   10.17 -  | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.to_string r ^ "\"");
   10.18 +  | rule2stac_inst thy r = raise ERROR ("rule2stac_inst: not applicable to \"" ^
   10.19 +      Rule.to_string (Proof_Context.init_global thy) r ^ "\"");
   10.20  
   10.21  (*for appropriate nesting take stacs in _reverse_ order*)
   10.22  fun op #>@ sts [s] = SEq $ s $ sts

    11.1 --- a/test/Tools/isac/Knowledge/rational-2.sml	Tue Jan 10 10:01:05 2023 +0100
    11.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml	Tue Jan 10 17:07:53 2023 +0100
    11.3 @@ -718,15 +718,15 @@
    11.4    (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)
    11.5  then () else error "first element of revset changed";
    11.6  if
    11.7 -(revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\", ?r1 \<up> 2 = ?r1 * ?r1)" andalso
    11.8 -(revsets |> nth 1 |> nth 2 |> Rule.to_string) = "Thm (\"#: 9 = 3 \<up> 2\", 9 = 3 \<up> 2)" andalso
    11.9 -(revsets |> nth 1 |> nth 3 |> Rule.to_string) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))"
   11.10 +(revsets |> nth 1 |> nth 1 |> Rule.to_string ctxt) = "Thm (\"realpow_twoI\", ?r1 \<up> 2 = ?r1 * ?r1)" andalso
   11.11 +(revsets |> nth 1 |> nth 2 |> Rule.to_string ctxt) = "Thm (\"#: 9 = 3 \<up> 2\", 9 = 3 \<up> 2)" andalso
   11.12 +(revsets |> nth 1 |> nth 3 |> Rule.to_string ctxt) = "Thm (\"#: 6 * x = 2 * (3 * x)\", 6 * x = 2 * (3 * x))"
   11.13  andalso
   11.14 -(revsets |> nth 1 |> nth 4 |> Rule.to_string) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))"
   11.15 +(revsets |> nth 1 |> nth 4 |> Rule.to_string ctxt) = "Thm (\"#: - 3 * x = - 1 * (3 * x)\", - 3 * x = - 1 * (3 * x))"
   11.16  andalso
   11.17 -(revsets |> nth 1 |> nth 5 |> Rule.to_string) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso
   11.18 -(revsets |> nth 1 |> nth 6 |> Rule.to_string) = "Rls_ (\"sym_order_mult_rls_\")" andalso
   11.19 -(revsets |> nth 1 |> nth 7 |> Rule.to_string) = 
   11.20 +(revsets |> nth 1 |> nth 5 |> Rule.to_string ctxt) = "Thm (\"#: 9 = 3 * 3\", 9 = 3 * 3)" andalso
   11.21 +(revsets |> nth 1 |> nth 6 |> Rule.to_string ctxt) = "Rls_ (\"sym_order_mult_rls_\")" andalso
   11.22 +(revsets |> nth 1 |> nth 7 |> Rule.to_string ctxt) = 
   11.23    "Thm (\"sym_mult.assoc\", ?a * (?b * ?c) = ?a * ?b * ?c)"
   11.24  then () else error "first 7 elements in revset changed"
   11.25  
   11.26 @@ -1581,7 +1581,7 @@
   11.27  
   11.28  (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1) der; (*default_print_depth 3;*)
   11.29  "...,(- 1 * b \<up> 2 + a \<up> 2) / (- 2 * (a * b) + a \<up> 2 + (- 1 * b) \<up> 2) ]";
   11.30 -(*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*)
   11.31 +(*default_print_depth 99;*) map ((Rule.to_string ctxt) o #2) der; (*default_print_depth 3;*)
   11.32  (*default_print_depth 99;*) map ((UnparseC.term_in_ctxt ctxt) o #1 o #3) der; (*default_print_depth 3;*)
   11.33  
   11.34  val der = Derive.do_one ctxt Atools_erls rules ro NONE