src/Tools/isac/Interpret/script.sml
branchdecompose-isar
changeset 41997 71704991fbb2
parent 41996 4e81dae36cab
child 41999 2d5a8c47f0c2
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Tue May 17 09:55:30 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Tue May 17 14:56:54 2011 +0200
     1.3 @@ -1709,7 +1709,7 @@
     1.4  			      "formals: " ^ terms2str formals ^ "\n" ^
     1.5  			      "actuals: " ^ terms2str actuals)
     1.6       val env = relate_args [] formals actuals;
     1.7 -   in (ScrState (env,[],NONE,e_term,Safe,true), e_ctxt, scr):istate * Proof.context * scr end;
     1.8 +   in (ScrState (env,[],NONE,e_term,Safe,true), (*FIXME.WN170511 remove*)e_ctxt, scr):istate * Proof.context * scr end;
     1.9  
    1.10  (* decide, where to get script/istate from:
    1.11     (*1*) from PblObj.env: at begin of script if no init_form