1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 25 16:30:15 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed Jun 13 07:28:39 2012 +0200
     1.3 @@ -1657,24 +1657,26 @@
     1.4      if is_spec_pos p_ 
     1.5      then [get_obj g_tac pt p]
     1.6      else
     1.7 -	let val pp = par_pblobj pt p
     1.8 -	    val thy' = (get_obj g_domID pt pp):theory'
     1.9 -	    val thy = assoc_thy thy'
    1.10 -	    val metID = get_obj g_metID pt pp
    1.11 -	    val metID' =if metID = e_metID 
    1.12 -			then (thd3 o snd3) (get_obj g_origin pt pp)
    1.13 -			else metID
    1.14 -	    val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
    1.15 -	    val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
    1.16 -	    val alltacs = (*we expect at least 1 stac in a script*)
    1.17 -		map ((stac2tac pt thy) o rep_stacexpr o #2 o
    1.18 -		     (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
    1.19 -	    val f = case p_ of
    1.20 -			Frm => get_obj g_form pt p
    1.21 -		      | Res => (fst o (get_obj g_result pt)) p
    1.22 -	(*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
    1.23 -	in (distinct o flat o 
    1.24 -	    (map (atomic_appl_tacs thy ro erls f))) alltacs end;
    1.25 +      let
    1.26 +        val pp = par_pblobj pt p
    1.27 +        val thy' = (get_obj g_domID pt pp):theory'
    1.28 +        val thy = assoc_thy thy'
    1.29 +        val metID = get_obj g_metID pt pp
    1.30 +        val metID' =
    1.31 +          if metID = e_metID 
    1.32 +          then (thd3 o snd3) (get_obj g_origin pt pp)
    1.33 +          else metID
    1.34 +        val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
    1.35 +        val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
    1.36 +        val alltacs = (*we expect at least 1 stac in a script*)
    1.37 +          map ((stac2tac pt thy) o rep_stacexpr o #2 o
    1.38 +           (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
    1.39 +        val f =
    1.40 +          case p_ of
    1.41 +              Frm => get_obj g_form pt p
    1.42 +            | Res => (fst o (get_obj g_result pt)) p
    1.43 +          (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
    1.44 +      in (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;
    1.45  	
    1.46  
    1.47  (*