1.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu Oct 06 17:03:44 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Mon Oct 10 18:24:14 2016 +0200
     1.3 @@ -522,8 +522,8 @@
     1.4  (*040214: version for concat_deriv*)
     1.5  fun rev_deriv' (t, r, (t', a)) = (t', sym_rule r, (t, a));
     1.6  
     1.7 -fun mk_tacis ro erls (t, r as Thm _, (t', a)) = 
     1.8 -      (Rewrite (rule2thm' r), 
     1.9 +fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) = 
    1.10 +      (Rewrite (id, Thm.prop_of thm), 
    1.11           Rewrite' ("Isac", fst ro, erls, false, rule2thm' r, t, (t', a)),
    1.12         (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
    1.13    | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) =