1.1 --- a/src/Tools/isac/Interpret/script.sml	Sat Aug 27 11:26:28 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Sat Aug 27 16:57:18 2016 +0200
     1.3 @@ -303,6 +303,8 @@
     1.4  !: FIXXXME penv: push it here in itms2args into script-evaluation*)
     1.5  (* val (thy, mI, itms) = (thy, metID, itms);
     1.6     *)
     1.7 +val errmsg = 
     1.8 +  "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
     1.9  fun itms2args thy mI (itms:itm list) =
    1.10      let val mvat = max_vt itms
    1.11  	fun okv mvat (_,vats,b,_,_) = member op = vats mvat andalso b
    1.12 @@ -317,6 +319,7 @@
    1.13  	      | SOME (_,_,_,_,itm_) => penvval_in itm_
    1.14  	fun sel_given_find (s,_) = (s = "#Given") orelse (s = "#Find")
    1.15  	val pats = (#ppc o get_met) mI
    1.16 +	val _ = if pats = [] then raise ERROR errmsg else ()
    1.17      in (flat o (map (itm2arg itms))) pats end;
    1.18  (*
    1.19  > val sc = ... Solve_root_equation ...
    1.20 @@ -1483,9 +1486,11 @@
    1.21  
    1.22  
    1.23  (*.create the initial interpreter state from the items of the guard.*)
    1.24 +val errmsg = "ERROR: found no actual arguments for prog. of "
    1.25  fun init_scrstate thy itms metID =
    1.26    let
    1.27      val actuals = itms2args thy metID itms
    1.28 +    val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
    1.29  	  val scr as Prog sc = (#scr o get_met) metID
    1.30      val formals = formal_args sc    
    1.31  	  (*expects same sequence of (actual) args in itms and (formal) args in met*)

     2.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Sat Aug 27 11:26:28 2016 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Sat Aug 27 16:57:18 2016 +0200
     2.3 @@ -93,7 +93,8 @@
     2.4            crls = e_rls, errpats = [], nrls = e_rls},
     2.5          "empty_script"),
     2.6      prep_met @{theory} "met_Programming" [] e_metID
     2.7 -      (["Programming","sort"], [],
     2.8 +      (["Programming","sort"], 
     2.9 +      [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
    2.10          {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = e_rls, prls = e_rls,
    2.11            crls = Atools_crls, errpats = [], nrls = norm_Rational},
    2.12          "Script Sortprog (unso :: int xlist) = " ^

     3.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml	Sat Aug 27 11:26:28 2016 +0200
     3.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Sat Aug 27 16:57:18 2016 +0200
     3.3 @@ -18,7 +18,7 @@
     3.4  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Problem",..*)
     3.5  "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
     3.6  val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (* (@1) nxt'''' = ("Specify_Method",..*)
     3.7 -(*val..nxt..*)me nxt'''' p'''' [] pt''''; (* nxt = ERROR("Empty_Tac", SHOULD BE("Apply_Method",..*)
     3.8 +(*me nxt'''' p'''' [] pt''''; "ERROR in creating the environment..", SHOULD BE("Apply_Method",.*)
     3.9  "~~~~~ we continue with (@1) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
    3.10  val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
    3.11  "~~~~~ fun me, args:"; val (_,tac) = nxt;