1.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu Oct 27 10:48:24 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Sat Nov 12 17:21:43 2016 +0100
     1.3 @@ -524,10 +524,10 @@
     1.4  
     1.5  fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) = 
     1.6        (Rewrite (id, thm), 
     1.7 -         Rewrite' ("Isac", fst ro, erls, false, rule2thm'' r, t, (t', a)),
     1.8 +         Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
     1.9         (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
    1.10    | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) = 
    1.11 -      (Rewrite_Set (rule2rls' r), 
    1.12 +      (Rewrite_Set (Lucin.rule2rls' r), 
    1.13           Rewrite_Set' ("Isac", false, rls, t, (t', a)),
    1.14         (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
    1.15    | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t);