1.1 --- a/src/Tools/isac/Interpret/generate.sml Thu Oct 06 17:03:44 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Mon Oct 10 18:24:14 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')) (f',asm) Complete;
1.12 + (Rewrite_Inst (subst2subs subs', (thm''_of_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 + | generate1 thy (Rewrite' (thy', ord', rls', pa, thm, f, (f', asm))) (is, ctxt) (p, p_) pt =
1.18 let
1.19 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.20 - (Rewrite thm') (f',asm) Complete
1.21 + (Rewrite (thm''_of_thm thm)) (f',asm) Complete
1.22 val pt = update_branch pt p TransitiveB
1.23 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.24