1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 20 08:32:57 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 20 09:12:40 2011 +0200
     1.3 @@ -1588,6 +1588,9 @@
     1.4  			      "actuals: " ^ terms2str actuals)
     1.5       val env = relate_args [] formals actuals;
     1.6       val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
     1.7 +     val {pre, prls, ...} = get_met metID;
     1.8 +     val pres = check_preconds thy prls pre itms |> map snd;
     1.9 +     (*val ctxt = ctxt |> insert_assumptions pres;*)
    1.10     in (ScrState (env,[],NONE,e_term,Safe,true), ctxt, scr):istate * Proof.context * scr end;
    1.11  
    1.12  (* decide, where to get script/istate from: