1.1 --- a/src/Tools/isac/Interpret/appl.sml	Thu Oct 06 17:03:44 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Mon Oct 10 18:24:14 2016 +0200
     1.3 @@ -357,7 +357,7 @@
     1.4    | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
     1.5    | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
     1.6  
     1.7 -  | applicable_in (p, p_) pt (m as Rewrite_Inst (subs, thm')) = 
     1.8 +  | applicable_in (p, p_) pt (m as Rewrite_Inst (subs, thm'')) = 
     1.9      if member op = [Pbl, Met] p_ 
    1.10      then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.11      else
    1.12 @@ -374,19 +374,20 @@
    1.13          let
    1.14            val subst = subs2subst thy subs;
    1.15            val subs' = subst2subs' subst;
    1.16 -        in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (assoc_thm' thy thm') f of
    1.17 +          val thm = assoc_thm'' thy thm''
    1.18 +        in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst thm f of
    1.19               SOME (f',asm) =>
    1.20 -               Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm', f, (f', asm)))
    1.21 -           | NONE => Notappl ((fst thm')^" not applicable")
    1.22 +               Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
    1.23 +           | NONE => Notappl (fst thm'' ^ " not applicable")
    1.24          end
    1.25          handle _ => Notappl ("syntax error in "^(subs2str subs))
    1.26        end
    1.27  
    1.28 -| applicable_in (p,p_) pt (m as Rewrite thm') = 
    1.29 +| applicable_in (p,p_) pt (m as Rewrite thm'') = 
    1.30    if member op = [Pbl,Met] p_ 
    1.31      then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.32    else
    1.33 -  let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
    1.34 +  let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm'' p pt;
    1.35      val thy = assoc_thy thy';
    1.36      val f = case p_ of
    1.37                Frm => get_obj g_form pt p
    1.38 @@ -397,16 +398,16 @@
    1.39       then
    1.40        ((*tracing("### applicable_in rls'= "^rls');*)
    1.41         (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
    1.42 -	  *)
    1.43 -       case rewrite_ thy (assoc_rew_ord ro) 
    1.44 -		     rls' false (assoc_thm' thy thm') f of
    1.45 -       SOME (f',asm) => Appl (
    1.46 -	   Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm)))
    1.47 -     | NONE => Notappl ("'"^(fst thm')^"' not applicable") )
    1.48 +	  *) 
    1.49 +	    let val thm = assoc_thm'' thy thm''
    1.50 +	    in case rewrite_ thy (assoc_rew_ord ro) rls' false thm f of
    1.51 +        SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
    1.52 +      | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable") 
    1.53 +      end)
    1.54       else Notappl msg
    1.55    end
    1.56  
    1.57 -| applicable_in (p,p_) pt (m as Rewrite_Asm thm') = 
    1.58 +| applicable_in (p,p_) pt (m as Rewrite_Asm thm'') = 
    1.59    if member op = [Pbl,Met] p_ 
    1.60      then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.61    else
    1.62 @@ -417,16 +418,16 @@
    1.63      val {rew_ord'=ro',erls=erls,...} = 
    1.64        get_met (get_obj g_metID pt pp);
    1.65      (*val put_asm = true;*)
    1.66 -    val (f,p) = case p_ of  (*p 12.4.00 unnecessary*)
    1.67 +    val (f, _) = case p_ of
    1.68                Frm => (get_obj g_form pt p, p)
    1.69  	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
    1.70  	    | _ => error ("applicable_in: call by "^
    1.71  				(pos'2str (p,p_)));
    1.72 -  in case rewrite_ thy (assoc_rew_ord ro') erls 
    1.73 -		   (*put_asm*)false (assoc_thm' thy thm') f of
    1.74 +    val thm = assoc_thm'' thy thm''
    1.75 +  in case rewrite_ thy (assoc_rew_ord ro') erls false thm f of
    1.76         SOME (f',asm) => Appl (
    1.77 -	   Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))
    1.78 -     | NONE => Notappl ("'"^(fst thm')^"' not applicable") end
    1.79 +	   Rewrite' (thy', ro', erls, false, thm, f, (f', asm)))
    1.80 +     | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end
    1.81  
    1.82    | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) = 
    1.83    if member op = [Pbl,Met] p_