1.1 --- a/src/Tools/isac/Interpret/generate.sml Tue Oct 18 12:05:03 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu Oct 20 10:26:29 2016 +0200
1.3 @@ -334,14 +334,14 @@
1.4 | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm', f, (f', asm))) (is, ctxt) (p,p_) pt =
1.5 let
1.6 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.7 - (Rewrite_Inst (subst2subs subs', thm'_to_thm'' thm')) (f',asm) Complete;
1.8 + (Rewrite_Inst (subst2subs subs', thm')) (f',asm) Complete;
1.9 val pt = update_branch pt p TransitiveB
1.10 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.11
1.12 | generate1 thy (Rewrite' (thy', ord', rls', pa, thm', f, (f', asm))) (is, ctxt) (p, p_) pt =
1.13 let
1.14 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.15 - (Rewrite (thm'_to_thm'' thm')) (f',asm) Complete
1.16 + (Rewrite thm') (f',asm) Complete
1.17 val pt = update_branch pt p TransitiveB
1.18 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.19