33 val pres = check_preconds thy prls pre meth |> map snd; |
33 val pres = check_preconds thy prls pre meth |> map snd; |
34 val ctxt = ctxt |> insert_assumptions pres; |
34 val ctxt = ctxt |> insert_assumptions pres; |
35 val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI; |
35 val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI; |
36 "~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI) |
36 "~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI) |
37 val actuals = itms2args thy metID itms |
37 val actuals = itms2args thy metID itms |
38 val scr as Script sc = (#scr o get_met) metID |
38 val scr as Prog sc = (#scr o get_met) metID |
39 val formals = formal_args sc |
39 val formals = formal_args sc |
40 (*expects same sequence of (actual) args in itms and (formal) args in met*) |
40 (*expects same sequence of (actual) args in itms and (formal) args in met*) |
41 fun relate_args env [] [] = env |
41 fun relate_args env [] [] = env |
42 | relate_args env _ [] = |
42 | relate_args env _ [] = |
43 error ("ERROR in creating the environment for '" ^ |
43 error ("ERROR in creating the environment for '" ^ |