1.1 --- a/src/Tools/isac/Interpret/inform.sml	Mon Jul 28 17:06:16 2014 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu Jul 31 14:15:41 2014 +0200
     1.3 @@ -521,7 +521,7 @@
     1.4  > *** dropwhile': did not start with equal elements*)
     1.5  
     1.6  (*040214: version for concat_deriv*)
     1.7 -fun rev_deriv' (t, r, (t', a)) = (t', sym_Thm r, (t, a));
     1.8 +fun rev_deriv' (t, r, (t', a)) = (t', sym_rule r, (t, a));
     1.9  
    1.10  fun mk_tacis ro erls (t, r as Thm _, (t', a)) = 
    1.11        (Rewrite (rule2thm' r),