1.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml	Mon Apr 27 16:40:11 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Tue Apr 28 15:31:49 2020 +0200
     1.3 @@ -27,7 +27,6 @@
     1.4  struct
     1.5  (**)
     1.6  
     1.7 -(*/------- to State_Steps from Generate -------\*)
     1.8  (* a single holds alle information required to build a node in the calc-tree;
     1.9     a single is assumed to be used efficiently such that the calc-tree
    1.10     resulting from applying a single need not be stored separately;
    1.11 @@ -53,8 +52,7 @@
    1.12  fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
    1.13    | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
    1.14    | result (_, tac_, _) = error ("result: called with" ^ Tactic.string_of tac_)
    1.15 -(*\------- to State_Steps from Generate -------/*)
    1.16 -(*/------- to State_Steps from Error_Pattern -------\*)
    1.17 +
    1.18  fun make_single ro erls (t, r as Rule.Thm (id, thm), (t', a)) = 
    1.19        (Tactic.Rewrite (id, thm), 
    1.20          Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, ThmC.from_rule r, t, (t', a)),
    1.21 @@ -64,7 +62,6 @@
    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 _ _ (t, r, _) = error ("make_single: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
    1.25 -(*\------- to State_Steps from Error_Pattern -------/*)
    1.26  
    1.27  (* update pos in tacis for embedding by generate *)
    1.28  fun insert_pos (_: Pos.pos) [] = []