1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri Aug 26 12:25:03 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Sat Aug 27 05:04:53 2016 +0200
     1.3 @@ -486,7 +486,13 @@
     1.4  local infix mem;
     1.5  fun x mem [] = false
     1.6    | x mem (y :: ys) = x = y orelse x mem ys;
     1.7 -in 
     1.8 +in
     1.9 +(*args of nxt_add
    1.10 +  thy : for?
    1.11 +  oris: from formalization 'type fmz', structured for efficient access 
    1.12 +  pbt : the problem-pattern to be matched with oris in order to get itms
    1.13 +  itms: already input items
    1.14 +*)
    1.15  fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
    1.16    let
    1.17      fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0; 
    1.18 @@ -529,7 +535,7 @@
    1.19  	 case find_first (test_subset (hd icl)) vors of
    1.20  	     (* val SOME ori = find_first (test_subset (hd icl)) vors;
    1.21  	      *)
    1.22 -	     NONE => error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
    1.23 +	     NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
    1.24  	   | SOME ori => SOME (geti_ct thy ori (hd icl))
    1.25    end
    1.26  end;