1.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml	Mon Jan 09 16:11:17 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml	Mon Jan 09 16:40:54 2023 +0100
     1.3 @@ -12,11 +12,11 @@
     1.4    datatype program = datatype Rule_Def.program
     1.5  
     1.6    val set_id: Rule_Def.rule_set -> string
     1.7 -  val id: Rule_Def.rule -> string
     1.8 -  val equal: Rule_Def.rule * Rule_Def.rule -> bool
     1.9 -  val to_string: Rule_Def.rule -> string
    1.10 +  val id: rule -> string
    1.11 +  val equal: rule * rule -> bool
    1.12 +  val to_string: rule -> string
    1.13    val to_string_PIDE: Proof.context -> rule -> string
    1.14 -  val to_string_short: Rule_Def.rule -> string
    1.15 +  val to_string_short: rule -> string
    1.16    val s_to_string: rule list -> string
    1.17  
    1.18    val thm: rule -> thm

     2.1 --- a/src/Tools/isac/Interpret/derive.sml	Mon Jan 09 16:11:17 2023 +0100
     2.2 +++ b/src/Tools/isac/Interpret/derive.sml	Mon Jan 09 16:40:54 2023 +0100
     2.3 @@ -100,7 +100,7 @@
     2.4            (case Rewrite.rewrite_set_ ctxt true rls t of
     2.5              NONE => rew_once lim rts t apno rs'
     2.6            | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
     2.7 -        | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule))
     2.8 +        | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string_PIDE ctxt rule))
     2.9      | rew_or_calc _ _ _ _ [] = raise ERROR "rew_or_calc: called with []"
    2.10    in rew_once (Config.get ctxt rewrite_limit) [] tt Noap rs end
    2.11  

     3.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Jan 09 16:11:17 2023 +0100
     3.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Mon Jan 09 16:40:54 2023 +0100
     3.3 @@ -207,7 +207,7 @@
     3.4              (case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of
     3.5                SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
     3.6              | NONE => rew_once ruls asm ct apno thms)
     3.7 -          | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
     3.8 +          | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string_PIDE ctxt r ^ "\"");
     3.9        val ruls = (#rules o Rule_Set.rep) rls;
    3.10        val _ = trace_eq1 ctxt i "rls" rls ct
    3.11        val (ct', asm') = rew_once ruls [] ct Noap ruls;

     4.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Mon Jan 09 16:11:17 2023 +0100
     4.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Mon Jan 09 16:40:54 2023 +0100
     4.3 @@ -57,7 +57,7 @@
     4.4        Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
     4.5       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
     4.6    | make_single ctxt _ _ (t, r, _) = raise ERROR ("State_Steps.make_single: not impl. for " ^
     4.7 -    Rule.to_string r ^ " at " ^ UnparseC.term_in_ctxt ctxt t)
     4.8 +    Rule.to_string_PIDE ctxt r ^ " at " ^ UnparseC.term_in_ctxt ctxt t)
     4.9  
    4.10  (* update pos in tacis for embedding by generate *)
    4.11  fun insert_pos (_: Pos.pos) [] = []

     5.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml	Mon Jan 09 16:11:17 2023 +0100
     5.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml	Mon Jan 09 16:40:54 2023 +0100
     5.3 @@ -259,8 +259,8 @@
     5.4    | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
     5.5    | rule2tac ctxt subst (Rule.Rls_ rls) = 
     5.6      Rewrite_Set_Inst (Subst.T_to_input ctxt subst, (Rule_Set.id rls))
     5.7 -  | rule2tac _ _ rule = 
     5.8 -    raise ERROR ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
     5.9 +  | rule2tac ctxt _ rule = 
    5.10 +    raise ERROR ("rule2tac: called with \"" ^ Rule.to_string_PIDE ctxt rule ^ "\"");
    5.11  
    5.12  (* try if a rewrite-rule is applicable to a given formula; 
    5.13     in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 

     6.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Mon Jan 09 16:11:17 2023 +0100
     6.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Mon Jan 09 16:40:54 2023 +0100
     6.3 @@ -165,7 +165,9 @@
     6.4            val id'' = Thm.get_name_hint thm'      (*recover the thy the thm comes from*)
     6.5          in Rule.Thm (id'', thm') end
     6.6        else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*)
     6.7 -  | revert_sym_rule _ rule = raise ERROR ("revert_sym_rule: NOT for " ^ Rule.to_string rule)
     6.8 +  | revert_sym_rule thy rule =
     6.9 +    raise ERROR ("ThmC.revert_sym_rule: NOT for " ^
    6.10 +      Rule.to_string_PIDE (Proof_Context.init_global thy) rule)
    6.11  \<close>
    6.12  
    6.13