1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Oct 30 14:40:22 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Oct 30 16:46:05 2019 +0100
     1.3 @@ -210,10 +210,8 @@
     1.4  		        val d = e_rls;
     1.5  (*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;
     1.6    WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
     1.7 -"~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'), 
     1.8 -	                                   (scr as Prog (h $ body),d), (Pstate (E,l,rls,a,v,S,b), ctxt)) = 
     1.9 -                                   ((thy',srls), m  ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_input_tactic 2nd pattern *)
    1.10 -val thy = assoc_thy thy';
    1.11 +"~~~~~ fun locate_input_tactic, args:"; val () = ();
    1.12 +(*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
    1.13  l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
    1.14  (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
    1.15    ... Assoc ... is correct*)
    1.16 @@ -249,6 +247,7 @@
    1.17  term2str consts';
    1.18  if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
    1.19  (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
    1.20 +( *----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------//*)
    1.21  
    1.22  "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";
    1.23  "----------- equality (2 +(-1)*x + x^^^2 = (0::real)) ----------------------------------------";