1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Sun Jan 08 16:19:31 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Sun Jan 08 17:26:00 2023 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4    val keep_unique_rules: string -> T ->  Rule_Def.rule list -> T
     1.5    val merge: string -> T -> T -> T
     1.6    val get_rules: T -> Rule_Def.rule list
     1.7 -  val id_from_rule: Rule.rule -> string
     1.8 +  val id_from_rule: Proof.context -> Rule.rule -> string
     1.9    val contains: Rule.rule -> T -> bool
    1.10  
    1.11  (*type for_know_store*)
    1.12 @@ -182,8 +182,9 @@
    1.13    | get_rules (Rule_Def.Sequence {rules, ...}) = rules
    1.14    | get_rules (Rule_Def.Rrls _) = [];
    1.15  
    1.16 -fun id_from_rule (Rule.Rls_ rls) = id rls
    1.17 -  | id_from_rule r = raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string r);
    1.18 +fun id_from_rule _ (Rule.Rls_ rls) = id rls
    1.19 +  | id_from_rule ctxt r =
    1.20 +    raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string_PIDE ctxt r);
    1.21  
    1.22  (* check if a rule is contained in a rule-set (recursivley down in Rls_);
    1.23     this rule can even be a rule-set itself                             *)

     2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Sun Jan 08 16:19:31 2023 +0100
     2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Sun Jan 08 17:26:00 2023 +0100
     2.3 @@ -626,7 +626,7 @@
     2.4      if found
     2.5      then
     2.6         let
     2.7 -         val tacis' = map (State_Steps.make_single rew_ord asm_rls) der;
     2.8 +         val tacis' = map (State_Steps.make_single ctxt rew_ord asm_rls) der;
     2.9  		     val (c', ptp) = Derive.embed tacis' ptp;
    2.10  	     in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
    2.11       else 

     3.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Sun Jan 08 16:19:31 2023 +0100
     3.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Sun Jan 08 17:26:00 2023 +0100
     3.3 @@ -815,7 +815,7 @@
     3.4          in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P) end
     3.5  	  end;
     3.6  
     3.7 -(* get the theory explicitly specified for the rootpbl;
     3.8 +(* get the theory explicitly just for the rootpbl;
     3.9     thus use this function _after_ finishing specification *)
    3.10  fun root_thy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Know_Store.get_via_last_thy thyID
    3.11    | root_thy _ = raise ERROR "root_thy: uncovered fun def.";

     4.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Sun Jan 08 16:19:31 2023 +0100
     4.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Sun Jan 08 17:26:00 2023 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4    type T
     4.5    val to_string : Proof.context -> T -> string
     4.6    val result : single -> (term * term list)
     4.7 -  val make_single: Rewrite_Ord.id * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
     4.8 +  val make_single: Proof.context -> Rewrite_Ord.id * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
     4.9      single
    4.10    val insert_pos : Pos.pos -> T -> T
    4.11  end
    4.12 @@ -48,15 +48,16 @@
    4.13    | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
    4.14    | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_)
    4.15  
    4.16 -fun make_single ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) = 
    4.17 +fun make_single _ ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) = 
    4.18        (Tactic.Rewrite (id, thm), 
    4.19          Tactic.Rewrite' ("Isac_Knowledge", fst ro, asm_rls, false, ThmC.from_rule r, t, (t', a)),
    4.20         (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    4.21 -  | make_single _ _ (t, r as Rule.Rls_ rls, (t', a)) = 
    4.22 -      (Tactic.Rewrite_Set (Rule_Set.id_from_rule r), 
    4.23 +  | make_single ctxt _ _ (t, r as Rule.Rls_ rls, (t', a)) = 
    4.24 +      (Tactic.Rewrite_Set (Rule_Set.id_from_rule ctxt r), 
    4.25          Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
    4.26         (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    4.27 -  | make_single _ _ (t, r, _) = raise ERROR ("make_single: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
    4.28 +  | make_single ctxt _ _ (t, r, _) = raise ERROR ("make_single: not impl. for " ^ Rule.to_string r ^
    4.29 +      " at " ^ UnparseC.term_in_ctxt ctxt t)
    4.30  
    4.31  (* update pos in tacis for embedding by generate *)
    4.32  fun insert_pos (_: Pos.pos) [] = []

     5.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Sun Jan 08 16:19:31 2023 +0100
     5.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml	Sun Jan 08 17:26:00 2023 +0100
     5.3 @@ -149,7 +149,7 @@
     5.4  (*\\------------------ step into Derive.steps ----------------------------------------------//*)
     5.5  
     5.6      (*if*) found (*then*);
     5.7 -         val tacis' = map (State_Steps.make_single rew_ord asm_rls) der;
     5.8 +         val tacis' = map (State_Steps.make_single ctxt rew_ord asm_rls) der;
     5.9  
    5.10  		     val (c', ptp) =
    5.11      Derive.embed tacis' ptp;