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;

     2.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Fri Aug 26 12:25:03 2016 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Sat Aug 27 05:04:53 2016 +0200
     2.3 @@ -3,17 +3,17 @@
     2.4  
     2.5  subsection {* consts *}
     2.6  consts
     2.7 -  unsorted   :: "'a list => unl"
     2.8 -  sorted     :: "'a list => unl"
     2.9 +  unsorted   :: "int xlist => unl"
    2.10 +  sorted     :: "int xlist => unl"
    2.11  
    2.12  (* subproblem and script-name *)
    2.13 -  Ins'_sort  :: "['a xlist,  
    2.14 -		    'a xlist] => 'a xlist"
    2.15 +  Ins'_sort  :: "[int xlist,  
    2.16 +		    int xlist] => int xlist"
    2.17                 ("((Script Ins'_sort (_ =))//  
    2.18  		    (_))" 9)
    2.19 -  Sort       :: "['a xlist,  
    2.20 -		    'a xlist] => 'a xlist"
    2.21 -               ("((Script Sort (_ =))//  
    2.22 +  Sortprog   :: "[int xlist,  
    2.23 +		    int xlist] => int xlist"
    2.24 +               ("((Script Sortprog (_ =))//  
    2.25  		    (_))" 9)
    2.26  
    2.27  subsection {* functions *}
    2.28 @@ -96,7 +96,7 @@
    2.29        (["Programming","sort"], [],
    2.30          {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = e_rls, prls = e_rls,
    2.31            crls = Atools_crls, errpats = [], nrls = norm_Rational},
    2.32 -        "Script Sort (u_u::'a xlist) = (Rewrite_Set ins_sort False) u_u")
    2.33 +        "Script Sortprog (u_u::int xlist) = (Rewrite_Set ins_sort False) u_u")
    2.34    ]
    2.35  *}
    2.36  end