1.1 --- a/src/Tools/isac/Interpret/derive.sml	Sun Jan 08 17:26:00 2023 +0100
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Mon Jan 09 16:11:17 2023 +0100
     1.3 @@ -107,14 +107,14 @@
     1.4  
     1.5  (** concatenate several steps in revers order **)
     1.6  
     1.7 -fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
     1.8 +fun rev_deriv ctxt (t, r, (_, a)) = (ThmC.make_sym_rule ctxt r, (t, a));
     1.9  fun steps_reverse ctxt asm_rls rs ro goal t =
    1.10 -    (rev o (map rev_deriv)) (do_one ctxt asm_rls rs ro goal t)
    1.11 +    (rev o (map (rev_deriv ctxt))) (do_one ctxt asm_rls rs ro goal t)
    1.12  
    1.13  
    1.14  (** concatenate several steps **)
    1.15  
    1.16 -fun rev_deriv' ctxt (t, r, (t', a)) = (t', ThmC.make_sym_rule_PIDE ctxt r, (t, a));
    1.17 +fun rev_deriv' ctxt (t, r, (t', a)) = (t', ThmC.make_sym_rule ctxt r, (t, a));
    1.18  
    1.19  (* case fo = ifo excluded already in inform *)
    1.20  fun steps ctxt rew_ord asm_rls rules fo ifo =

     2.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Sun Jan 08 17:26:00 2023 +0100
     2.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Mon Jan 09 16:11:17 2023 +0100
     2.3 @@ -48,16 +48,16 @@
     2.4    | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
     2.5    | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_)
     2.6  
     2.7 -fun make_single _ ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) = 
     2.8 -      (Tactic.Rewrite (id, thm), 
     2.9 -        Tactic.Rewrite' ("Isac_Knowledge", fst ro, asm_rls, false, ThmC.from_rule r, t, (t', a)),
    2.10 -       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    2.11 +fun make_single ctxt ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) = 
    2.12 +    (Tactic.Rewrite (id, thm), 
    2.13 +      Tactic.Rewrite' ("Isac_Knowledge", fst ro, asm_rls, false, ThmC.from_rule ctxt r, t, (t', a)),
    2.14 +     (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    2.15    | make_single ctxt _ _ (t, r as Rule.Rls_ rls, (t', a)) = 
    2.16 -      (Tactic.Rewrite_Set (Rule_Set.id_from_rule ctxt r), 
    2.17 -        Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
    2.18 -       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    2.19 -  | make_single ctxt _ _ (t, r, _) = raise ERROR ("make_single: not impl. for " ^ Rule.to_string r ^
    2.20 -      " at " ^ UnparseC.term_in_ctxt ctxt t)
    2.21 +    (Tactic.Rewrite_Set (Rule_Set.id_from_rule ctxt r), 
    2.22 +      Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
    2.23 +     (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    2.24 +  | make_single ctxt _ _ (t, r, _) = raise ERROR ("State_Steps.make_single: not impl. for " ^
    2.25 +    Rule.to_string r ^ " at " ^ UnparseC.term_in_ctxt ctxt t)
    2.26  
    2.27  (* update pos in tacis for embedding by generate *)
    2.28  fun insert_pos (_: Pos.pos) [] = []

     3.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Sun Jan 08 17:26:00 2023 +0100
     3.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Mon Jan 09 16:11:17 2023 +0100
     3.3 @@ -23,23 +23,21 @@
     3.4  
     3.5    val id_of_thm: thm -> id
     3.6    val of_thm: thm -> T
     3.7 -  val from_rule : Rule.rule -> T
     3.8 +  val from_rule : Proof.context -> Rule.rule -> T
     3.9    val member': id list -> Rule.rule -> bool
    3.10  
    3.11    val is_sym: id -> bool
    3.12    val thm_from_thy: theory -> id -> thm
    3.13  
    3.14 -  val revert_sym_rule: theory -> Rule.rule -> Rule.rule
    3.15 -
    3.16    val make_rule: Proof.context -> bool -> string * Position.T -> Rule_Def.rule
    3.17  
    3.18  \<^isac_test>\<open>
    3.19    val dest_eq_concl: thm -> term * term
    3.20    val string_of_thm_in_thy: theory -> thm -> string
    3.21    val id_drop_sym: id -> id
    3.22 +  val revert_sym_rule: theory -> Rule.rule -> Rule.rule
    3.23  \<close>
    3.24 -  val make_sym_rule_PIDE: Proof.context -> Rule.rule -> Rule.rule
    3.25 -  val make_sym_rule: Rule.rule -> Rule.rule
    3.26 +  val make_sym_rule: Proof.context -> Rule.rule -> Rule.rule
    3.27    val make_sym_rule_set: Rule_Set.T -> Rule_Set.T
    3.28    val sym_thm: thm -> thm
    3.29  end
    3.30 @@ -65,8 +63,10 @@
    3.31  
    3.32  fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id;
    3.33  fun of_thm thm = (id_of_thm thm, thm);
    3.34 -fun from_rule (Rule.Thm (id, thm)) = (id, thm)
    3.35 -  | from_rule r = raise ERROR ("rule2thm': not defined for " ^ Rule.to_string r);
    3.36 +fun from_rule _ (Rule.Thm (id, thm)) = (id, thm)
    3.37 +  | from_rule ctxt r =
    3.38 +    raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string_PIDE ctxt r);
    3.39 +
    3.40  \<^isac_test>\<open>
    3.41  fun string_of_thm_in_thy thy thm =
    3.42    UnparseC.term_in_ctxt (Proof_Context.init_global thy) (Thm.prop_of thm);
    3.43 @@ -142,7 +142,7 @@
    3.44        prepat = prepat, rew_ord = rew_ord}
    3.45  
    3.46  (* toggles sym_* and keeps "#:" for ad-hoc theorems *)
    3.47 -fun make_sym_rule_PIDE ctxt (Rule.Thm (thmID, thm)) =
    3.48 +fun make_sym_rule ctxt (Rule.Thm (thmID, thm)) =
    3.49        let
    3.50          val thm' = sym_thm thm
    3.51          val thmID' = case Symbol.explode thmID of
    3.52 @@ -150,19 +150,10 @@
    3.53          | "#" :: ":" :: _ => "#: " ^ string_of_thm_PIDE ctxt thm'
    3.54          | _ => "sym_" ^ thmID
    3.55        in Rule.Thm (thmID', thm') end
    3.56 -  | make_sym_rule_PIDE _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
    3.57 -  | make_sym_rule_PIDE ctxt r = raise ERROR ("make_sym_rule: not for " ^  Rule.to_string_PIDE ctxt r)
    3.58 -fun make_sym_rule (Rule.Thm (thmID, thm)) =
    3.59 -      let
    3.60 -        val thm' = sym_thm thm
    3.61 -        val thmID' = case Symbol.explode thmID of
    3.62 -          "s" :: "y" :: "m" :: "_" :: id => implode id
    3.63 -        | "#" :: ":" :: _ => "#: " ^ string_of_thm thm'
    3.64 -        | _ => "sym_" ^ thmID
    3.65 -      in Rule.Thm (thmID', thm') end
    3.66 -  | make_sym_rule (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
    3.67 -  | make_sym_rule r = raise ERROR ("make_sym_rule: not for " ^  Rule.to_string r)
    3.68 +  | make_sym_rule _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
    3.69 +  | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^  Rule.to_string_PIDE ctxt r)
    3.70  
    3.71 +\<^isac_test>\<open>
    3.72  (* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *)
    3.73  fun revert_sym_rule thy (Rule.Thm (id, thm)) =
    3.74                              (*this ^^ might come from the user, who doesn't care about thy*)
    3.75 @@ -175,6 +166,7 @@
    3.76          in Rule.Thm (id'', thm') end
    3.77        else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*)
    3.78    | revert_sym_rule _ rule = raise ERROR ("revert_sym_rule: NOT for " ^ Rule.to_string rule)
    3.79 +\<close>
    3.80  
    3.81  
    3.82  (* ML antiquotations *)

     4.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Sun Jan 08 17:26:00 2023 +0100
     4.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Mon Jan 09 16:11:17 2023 +0100
     4.3 @@ -130,14 +130,14 @@
     4.4            val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
     4.5  
     4.6  (*/--- local to steps ---\*)
     4.7 -fun rev_deriv' ctxt (t, r, (t', a)) = (t', ThmC.make_sym_rule_PIDE ctxt r, (t, a));
     4.8 +fun rev_deriv' ctxt (t, r, (t', a)) = (t', ThmC.make_sym_rule ctxt r, (t, a));
     4.9  (*\--- local to steps ---/*)
    4.10  val return = (true, fod' @ (map
    4.11            (rev_deriv' ctxt) rifod'));
    4.12  "~~~~~ fun rev_deriv' , args:"; val (ctxt, (t, r, (t', a))) = (ctxt, nth 1 rifod');
    4.13  
    4.14  val return = (t',
    4.15 -      ThmC.make_sym_rule_PIDE ctxt r, (t, a));
    4.16 +      ThmC.make_sym_rule ctxt r, (t, a));
    4.17  "~~~~~ fun make_sym_rule_PIDE , args:"; val (ctxt ,(Rule.Thm (thmID, thm))) = (ctxt, r);
    4.18  open ThmC
    4.19          val thm' = sym_thm thm