diff -r 12dffe6c0a8b -r 727dff4f6b2c src/Tools/isac/Interpret/generate.sml
--- a/src/Tools/isac/Interpret/generate.sml	Thu Oct 06 17:03:44 2016 +0200
+++ b/src/Tools/isac/Interpret/generate.sml	Mon Oct 10 18:24:14 2016 +0200
@@ -331,17 +331,17 @@
         val (pt,c) = append_result pt p' l tasm Complete;
       in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
 
-  | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f', asm))) (is, ctxt) (p,p_) pt =
+  | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm, f, (f', asm))) (is, ctxt) (p,p_) pt =
       let
         val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
-          (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
+          (Rewrite_Inst (subst2subs subs', (thm''_of_thm thm))) (f', asm) Complete;
         val pt = update_branch pt p TransitiveB
       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
 
-  | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt) (p,p_) pt =
+  | generate1 thy (Rewrite' (thy', ord', rls', pa, thm, f, (f', asm))) (is, ctxt) (p, p_) pt =
       let
         val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
-          (Rewrite thm') (f',asm) Complete
+          (Rewrite (thm''_of_thm thm)) (f',asm) Complete
         val pt = update_branch pt p TransitiveB
       in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end