1.1 --- a/src/Tools/isac/Interpret/inform.sml	Tue Oct 18 12:05:03 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu Oct 20 10:26:29 2016 +0200
     1.3 @@ -523,13 +523,14 @@
     1.4  fun rev_deriv' (t, r, (t', a)) = (t', sym_rule r, (t, a));
     1.5  
     1.6  fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) = 
     1.7 -      (Rewrite (id, Thm.prop_of thm), 
     1.8 -         Rewrite' ("Isac", fst ro, erls, false, rule2thm' r, t, (t', a)),
     1.9 +      (Rewrite (id, thm), 
    1.10 +         Rewrite' ("Isac", fst ro, erls, false, rule2thm'' r, t, (t', a)),
    1.11         (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
    1.12 -  | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) = 
    1.13 +  | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) = 
    1.14        (Rewrite_Set (rule2rls' r), 
    1.15           Rewrite_Set' ("Isac", false, rls, t, (t', a)),
    1.16 -       (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)));
    1.17 +       (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
    1.18 +  | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t);
    1.19  
    1.20  (*fo = ifo excluded already in inform*)
    1.21  fun concat_deriv rew_ord erls rules fo ifo =