1.1 --- a/src/Tools/isac/Interpret/script.sml	Tue Sep 14 15:46:56 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Sep 23 08:43:36 2010 +0200
     1.3 @@ -448,12 +448,14 @@
     1.4  	val (pI, pors, mI) = 
     1.5  	    if mI = ["no_met"] 
     1.6  	    then let val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
     1.7 -			 handle _ =>(match_ags_msg pI stac ags(*raise exn*);[])
     1.8 +			 handle ERROR "actual args do not match formal args" 
     1.9 +				=> (match_ags_msg pI stac ags(*raise exn*);[])
    1.10  		     val pI' = refine_ori' pors pI;
    1.11  		 in (pI', pors (*refinement over models with diff.prec only*), 
    1.12  		     (hd o #met o get_pbt) pI') end
    1.13  	    else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
    1.14 -		  handle _ => (match_ags_msg pI stac ags(*raise exn*); []), 
    1.15 +		  handle ERROR "actual args do not match formal args"
    1.16 +			 => (match_ags_msg pI stac ags(*raise exn*); []), 
    1.17  		  mI);
    1.18          val (fmz_, vals) = oris2fmz_vals pors;
    1.19  	val {cas,ppc,thy,...} = get_pbt pI
    1.20 @@ -714,12 +716,14 @@
    1.21  	val (pI, pors, mI) = 
    1.22  	    if mI = ["no_met"] 
    1.23  	    then let val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
    1.24 -			 handle _=>(match_ags_msg pI stac ags(*raise exn*);[]);
    1.25 +			 handle ERROR "actual args do not match formal args"
    1.26 +				=> (match_ags_msg pI stac ags(*raise exn*);[]);
    1.27  		     val pI' = refine_ori' pors pI;
    1.28  		 in (pI', pors (*refinement over models with diff.prec only*), 
    1.29  		     (hd o #met o get_pbt) pI') end
    1.30  	    else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
    1.31 -		      handle _ => (match_ags_msg pI stac ags(*raise exn*);[]), 
    1.32 +		      handle ERROR "actual args do not match formal args"
    1.33 +			     => (match_ags_msg pI stac ags(*raise exn*);[]), 
    1.34  		  mI);
    1.35          val (fmz_, vals) = oris2fmz_vals pors;
    1.36  	val {cas, ppc,...} = get_pbt pI