test/Tools/isac/Knowledge/polyeq-1.sml
changeset 59676 6c23dc07c454
parent 59666 f461cae19cd4
child 59679 7b3c7a3d89e8
     1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Sun Oct 27 12:10:57 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Oct 30 11:02:41 2019 +0100
     1.3 @@ -211,7 +211,7 @@
     1.4  (*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;
     1.5    WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
     1.6  "~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'), 
     1.7 -	                                   (scr as Prog (h $ body),d), (Pstate (E,l,a,v,S,b), ctxt)) = 
     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  l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);