1.1 --- a/src/Tools/isac/Interpret/generate.sml	Sun Oct 16 13:58:46 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Tue Oct 18 12:05:03 2016 +0200
     1.3 @@ -331,17 +331,17 @@
     1.4          val (pt,c) = append_result pt p' l tasm Complete;
     1.5        in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
     1.6  
     1.7 -  | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm, f, (f', asm))) (is, ctxt) (p,p_) pt =
     1.8 +  | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm', f, (f', asm))) (is, ctxt) (p,p_) pt =
     1.9        let
    1.10          val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    1.11 -          (Rewrite_Inst (subst2subs subs', (thm''_of_thm thm))) (f', asm) Complete;
    1.12 +          (Rewrite_Inst (subst2subs subs', thm'_to_thm'' thm')) (f',asm) Complete;
    1.13          val pt = update_branch pt p TransitiveB
    1.14        in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
    1.15 -
    1.16 -  | generate1 thy (Rewrite' (thy', ord', rls', pa, thm, f, (f', asm))) (is, ctxt) (p, p_) pt =
    1.17 + 
    1.18 + | generate1 thy (Rewrite' (thy', ord', rls', pa, thm', f, (f', asm))) (is, ctxt) (p, p_) pt =
    1.19        let
    1.20          val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    1.21 -          (Rewrite (thm''_of_thm thm)) (f',asm) Complete
    1.22 +          (Rewrite (thm'_to_thm'' thm')) (f',asm) Complete
    1.23          val pt = update_branch pt p TransitiveB
    1.24        in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
    1.25