1.1 --- a/src/Tools/isac/Interpret/appl.sml	Thu Jan 05 17:43:48 2012 +0100
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Sat Jan 07 10:06:06 2012 +0100
     1.3 @@ -549,44 +549,33 @@
     1.4    (2) Pattern.match: for solving equational systems 
     1.5        (which raises exn for ?a..?z)*)
     1.6    | applicable_in (p,p_) pt (m as Substitute sube) = 
     1.7 -  if member op = [Pbl,Met] p_ 
     1.8 -  then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
     1.9 -  else let val pp = par_pblobj pt p
    1.10 -	   val thy = assoc_thy (get_obj g_domID pt pp)
    1.11 -	   val f = case p_ of
    1.12 -		       Frm => get_obj g_form pt p
    1.13 -		     | Res => (fst o (get_obj g_result pt)) p
    1.14 -	   val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
    1.15 -	   val subte = sube2subte sube
    1.16 -	   val subst = sube2subst thy sube
    1.17 -       in if foldl and_ (true, map contains_Var subte)
    1.18 -	  (*1*)
    1.19 -	  then let val f' = subst_atomic subst f
    1.20 -	       in if f = f' then Notappl (sube2str sube^" not applicable")
    1.21 -		  else Appl (Substitute' (subte, f, f'))
    1.22 -	       end
    1.23 -	  (*2*)
    1.24 -	  else case rewrite_terms_ thy (assoc_rew_ord rew_ord') 
    1.25 -				   erls subte f of
    1.26 -		   SOME (f', _) =>  Appl (Substitute' (subte, f, f'))
    1.27 -		 | NONE => Notappl (sube2str sube^" not applicable")
    1.28 -       end
    1.29 -(*-------WN08114 interrupted with error in polyminus.sml "11 = 11"
    1.30 -  | applicable_in (p,p_) pt (m as Substitute sube) = 
    1.31 -  if member op = [Pbl,Met] p_ 
    1.32 -  then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.33 -  else let val pp = par_pblobj pt p
    1.34 -	   val thy = assoc_thy (get_obj g_domID pt pp)
    1.35 -	   val f = case p_ of
    1.36 -		       Frm => get_obj g_form pt p
    1.37 -		     | Res => (fst o (get_obj g_result pt)) p
    1.38 -	   val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
    1.39 -	   val subte = sube2subte sube
    1.40 -       in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of
    1.41 -	      SOME (f', _) =>  Appl (Substitute' (subte, f, f'))
    1.42 -	    | NONE => Notappl (sube2str sube^" not applicable")
    1.43 -       end
    1.44 -------------------*)
    1.45 +      if member op = [Pbl,Met] p_ 
    1.46 +      then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    1.47 +      else 
    1.48 +        let
    1.49 +          val pp = par_pblobj pt p
    1.50 +          val thy = assoc_thy (get_obj g_domID pt pp)
    1.51 +          val f = case p_ of
    1.52 +		        Frm => get_obj g_form pt p
    1.53 +		      | Res => (fst o (get_obj g_result pt)) p
    1.54 +		      val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
    1.55 +		      val subte = sube2subte sube
    1.56 +		      val subst = sube2subst thy sube
    1.57 +		      val ro = assoc_rew_ord rew_ord'
    1.58 +		    in
    1.59 +		      if foldl and_ (true, map contains_Var subte)
    1.60 +		      (*1*)
    1.61 +		      then
    1.62 +		        let val f' = subst_atomic subst f
    1.63 +		        in if f = f' then Notappl (sube2str sube^" not applicable")
    1.64 +		           else Appl (Substitute' (ro, erls, subte, f, f'))
    1.65 +		        end
    1.66 +		        (*2*)
    1.67 +		      else 
    1.68 +		        case rewrite_terms_ thy ro erls subte f of
    1.69 +		            SOME (f', _) =>  Appl (Substitute' (ro, erls, subte, f, f'))
    1.70 +		          | NONE => Notappl (sube2str sube^" not applicable")
    1.71 +		    end
    1.72  
    1.73    | applicable_in p pt (Apply_Assumption cts') = 
    1.74        (error ("applicable_in: not impl. for " ^ (tac2str (Apply_Assumption cts'))))