1.1 --- a/src/Tools/isac/Interpret/appl.sml	Sun Oct 16 13:58:46 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Tue Oct 18 12:05:03 2016 +0200
     1.3 @@ -374,11 +374,10 @@
     1.4          let
     1.5            val subst = subs2subst thy subs;
     1.6            val subs' = subst2subs' subst;
     1.7 -          val thm = assoc_thm'' thy thm''
     1.8 -        in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst thm f of
     1.9 +        in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (assoc_thm'' thy thm'') f of
    1.10               SOME (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 +               Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm''_to_thm' thm'', f, (f', asm)))
    1.14 +           | NONE => Notappl ((fst thm'')^" not applicable")
    1.15          end
    1.16          handle _ => Notappl ("syntax error in "^(subs2str subs))
    1.17        end
    1.18 @@ -396,14 +395,9 @@
    1.19  				(pos'2str (p,p_)));
    1.20    in if msg = "OK" 
    1.21       then
    1.22 -      ((*tracing("### applicable_in rls'= "^rls');*)
    1.23 -       (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
    1.24 -	  *) 
    1.25 -	    let val thm = assoc_thm'' thy thm''
    1.26 -	    in case rewrite_ thy (assoc_rew_ord ro) rls' false thm f of
    1.27 -        SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
    1.28 -      | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable") 
    1.29 -      end)
    1.30 +        case rewrite_ thy (assoc_rew_ord ro) rls' false (assoc_thm'' thy thm'') f of
    1.31 +         SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm''_to_thm' thm'', f, (f', asm)))
    1.32 +       | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable") 
    1.33       else Notappl msg
    1.34    end
    1.35  
    1.36 @@ -423,10 +417,9 @@
    1.37  	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
    1.38  	    | _ => error ("applicable_in: call by "^
    1.39  				(pos'2str (p,p_)));
    1.40 -    val thm = assoc_thm'' thy thm''
    1.41 -  in case rewrite_ thy (assoc_rew_ord ro') erls false thm f of
    1.42 +  in case rewrite_ thy (assoc_rew_ord ro') erls false (assoc_thm'' thy thm'') f of
    1.43         SOME (f',asm) => Appl (
    1.44 -	   Rewrite' (thy', ro', erls, false, thm, f, (f', asm)))
    1.45 +	   Rewrite' (thy', ro', erls, false, thm''_to_thm' thm'', f, (f', asm)))
    1.46       | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end
    1.47  
    1.48    | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =