1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed May 18 09:25:36 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed May 18 09:32:26 2011 +0200
     1.3 @@ -1217,9 +1217,6 @@
     1.4            NOT IMPL. -- "error: do other step before"
     1.5     NotLocatable: thus generate_hard
     1.6  *)
     1.7 -(* val (Rewrite'(_,ro,er,pa,(id,str),f,_), p, Rfuns {locate_rule=lo,...},
     1.8 -	RrlsState (_,f'',rss,rts)) = (m, (p,p_), sc, is);
     1.9 -   *)
    1.10  fun locate_gen (thy',_) (Rewrite'(_,ro,er,pa,(id,str),f,_)) (pt,p) 
    1.11  	       (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) = 
    1.12      (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of