1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 20 07:24:18 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 20 08:12:51 2011 +0200
     1.3 @@ -1555,11 +1555,11 @@
     1.4  
     1.5  
     1.6  (*.create the initial interpreter state from the items of the guard.*)
     1.7 -fun init_scrstate thy itms metID =(*FIXME.WN170511: delete ctxt from value*)
     1.8 +fun init_scrstate thy itms metID =
     1.9    let
    1.10 -    val actuals = itms2args thy metID itms;
    1.11 -	  val scr as Script sc = (#scr o get_met) metID;
    1.12 -    val formals = formal_args sc
    1.13 +    val actuals = itms2args thy metID itms
    1.14 +	  val scr as Script sc = (#scr o get_met) metID
    1.15 +    val formals = formal_args sc    
    1.16  	  (*expects same sequence of (actual) args in itms and (formal) args in met*)
    1.17  	  fun relate_args env [] [] = env
    1.18  	    | relate_args env _ [] = 
    1.19 @@ -1587,7 +1587,8 @@
    1.20  			      "formals: " ^ terms2str formals ^ "\n" ^
    1.21  			      "actuals: " ^ terms2str actuals)
    1.22       val env = relate_args [] formals actuals;
    1.23 -   in (ScrState (env,[],NONE,e_term,Safe,true), (*FIXME.WN170511 remove*)e_ctxt, scr):istate * Proof.context * scr end;
    1.24 +     val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
    1.25 +   in (ScrState (env,[],NONE,e_term,Safe,true), ctxt, scr):istate * Proof.context * scr end;
    1.26  
    1.27  (* decide, where to get script/istate from:
    1.28     (*1*) from PblObj.env: at begin of script if no init_form