1.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Sun Jan 08 17:26:00 2023 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Mon Jan 09 16:11:17 2023 +0100
     1.3 @@ -48,16 +48,16 @@
     1.4    | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
     1.5    | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_)
     1.6  
     1.7 -fun make_single _ ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) = 
     1.8 -      (Tactic.Rewrite (id, thm), 
     1.9 -        Tactic.Rewrite' ("Isac_Knowledge", fst ro, asm_rls, false, ThmC.from_rule r, t, (t', a)),
    1.10 -       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    1.11 +fun make_single ctxt ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) = 
    1.12 +    (Tactic.Rewrite (id, thm), 
    1.13 +      Tactic.Rewrite' ("Isac_Knowledge", fst ro, asm_rls, false, ThmC.from_rule ctxt r, t, (t', a)),
    1.14 +     (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    1.15    | make_single ctxt _ _ (t, r as Rule.Rls_ rls, (t', a)) = 
    1.16 -      (Tactic.Rewrite_Set (Rule_Set.id_from_rule ctxt r), 
    1.17 -        Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
    1.18 -       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    1.19 -  | make_single ctxt _ _ (t, r, _) = raise ERROR ("make_single: not impl. for " ^ Rule.to_string r ^
    1.20 -      " at " ^ UnparseC.term_in_ctxt ctxt t)
    1.21 +    (Tactic.Rewrite_Set (Rule_Set.id_from_rule ctxt r), 
    1.22 +      Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
    1.23 +     (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    1.24 +  | make_single ctxt _ _ (t, r, _) = raise ERROR ("State_Steps.make_single: not impl. for " ^
    1.25 +    Rule.to_string r ^ " at " ^ UnparseC.term_in_ctxt ctxt t)
    1.26  
    1.27  (* update pos in tacis for embedding by generate *)
    1.28  fun insert_pos (_: Pos.pos) [] = []