1.1 --- a/src/Tools/isac/Interpret/appl.sml	Tue Oct 18 12:05:03 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Thu Oct 20 10:26:29 2016 +0200
     1.3 @@ -374,9 +374,9 @@
     1.4          let
     1.5            val subst = subs2subst thy subs;
     1.6            val subs' = subst2subs' subst;
     1.7 -        in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (assoc_thm'' thy thm'') f of
     1.8 +        in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (snd thm'') f of
     1.9               SOME (f',asm) =>
    1.10 -               Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm''_to_thm' thm'', f, (f', asm)))
    1.11 +               Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
    1.12             | NONE => Notappl ((fst thm'')^" not applicable")
    1.13          end
    1.14          handle _ => Notappl ("syntax error in "^(subs2str subs))
    1.15 @@ -395,8 +395,8 @@
    1.16  				(pos'2str (p,p_)));
    1.17    in if msg = "OK" 
    1.18       then
    1.19 -        case rewrite_ thy (assoc_rew_ord ro) rls' false (assoc_thm'' thy thm'') f of
    1.20 -         SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm''_to_thm' thm'', f, (f', asm)))
    1.21 +        case rewrite_ thy (assoc_rew_ord ro) rls' false (snd thm'') f of
    1.22 +         SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
    1.23         | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable") 
    1.24       else Notappl msg
    1.25    end
    1.26 @@ -417,9 +417,9 @@
    1.27  	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
    1.28  	    | _ => error ("applicable_in: call by "^
    1.29  				(pos'2str (p,p_)));
    1.30 -  in case rewrite_ thy (assoc_rew_ord ro') erls false (assoc_thm'' thy thm'') f of
    1.31 +  in case rewrite_ thy (assoc_rew_ord ro') erls false (snd thm'') f of
    1.32         SOME (f',asm) => Appl (
    1.33 -	   Rewrite' (thy', ro', erls, false, thm''_to_thm' thm'', f, (f', asm)))
    1.34 +	   Rewrite' (thy', ro', erls, false, thm'', f, (f', asm)))
    1.35       | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end
    1.36  
    1.37    | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =