let val pp = par_pblobj pt p

       let

 	    val thy' = (get_obj g_domID pt pp):theory'

         val pp = par_pblobj pt p

 	    val thy = assoc_thy thy'

         val thy' = (get_obj g_domID pt pp):theory'

 	    val metID = get_obj g_metID pt pp

         val thy = assoc_thy thy'

 	    val metID' =if metID = e_metID 

         val metID = get_obj g_metID pt pp

 			then (thd3 o snd3) (get_obj g_origin pt pp)

         val metID' =

 			else metID

           if metID = e_metID 

 	    val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'

           then (thd3 o snd3) (get_obj g_origin pt pp)

 	    val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)

           else metID

 	    val alltacs = (*we expect at least 1 stac in a script*)

         val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'

 		map ((stac2tac pt thy) o rep_stacexpr o #2 o

         val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)

 		     (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)

         val alltacs = (*we expect at least 1 stac in a script*)

 	    val f = case p_ of

           map ((stac2tac pt thy) o rep_stacexpr o #2 o

 			Frm => get_obj g_form pt p

            (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)

 		      | Res => (fst o (get_obj g_result pt)) p

         val f =

 	(*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)

           case p_ of

 	in (distinct o flat o 

               Frm => get_obj g_form pt p

 	    (map (atomic_appl_tacs thy ro erls f))) alltacs end;

             | Res => (fst o (get_obj g_result pt)) p

           (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)

       in (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;