1.1 --- a/src/Tools/isac/Interpret/inform.sml	Tue May 22 07:00:53 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/inform.sml	Tue May 22 13:40:06 2012 +0200
     1.3 @@ -720,7 +720,7 @@
     1.4        rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
     1.5    in (*the fillpat of the thm must be dedicated to errpatID*)
     1.6      if errpatID = erpaID andalso rewritten
     1.7 -    then SOME (fillpatID, term2str (HOLogic.mk_eq (form, form'))) else NONE end;
     1.8 +    then SOME (fillpatID, HOLogic.mk_eq (form, form')) else NONE end;
     1.9  
    1.10  fun get_fillpats subst form errpatID thm =
    1.11        let