1.1 --- a/src/Tools/isac/Interpret/inform.sml	Tue Feb 04 16:45:36 2020 +0100
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Tue Feb 04 17:11:54 2020 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
     1.5    val find_fillpatterns : Calc.T -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
     1.6    val is_exactly_equal : Calc.T -> string -> string * Tactic.input
     1.7 -(*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
     1.8 +(*cp here from "! aktivate for Test_Isac" below due to Lucin*)
     1.9    val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
    1.10      Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
    1.11    val mk_tacis: Rule.rew_ord' * 'a -> Rule.rls -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))
    1.12 @@ -339,10 +339,10 @@
    1.13  
    1.14  fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) = 
    1.15        (Tactic.Rewrite (id, thm), 
    1.16 -        Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
    1.17 +        Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, LItool.rule2thm'' r, t, (t', a)),
    1.18         (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
    1.19    | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) = 
    1.20 -      (Tactic.Rewrite_Set (Lucin.rule2rls' r), 
    1.21 +      (Tactic.Rewrite_Set (LItool.rule2rls' 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.Uistate, ContextC.e_ctxt)))
    1.24    | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ Rule.term2str t)