# HG changeset patch
# User wenzelm
# Date 1210756571 -7200
# Node ID d43264d547f85387e746320ff9acd5b4a9d158ec
# Parent  cfd5eb1677064205c1d196a24819a832e59edb03
use_text: added str_of_pos argument (ignored);

diff -r cfd5eb167706 -r d43264d547f8 Admin/isatest/annomaly.ML
--- a/Admin/isatest/annomaly.ML	Wed May 14 11:09:07 2008 +0200
+++ b/Admin/isatest/annomaly.ML	Wed May 14 11:16:11 2008 +0200
@@ -44,7 +44,7 @@
 
 in
 
-  fun use_text tune (line, name) p v t =
+  fun use_text tune str_of_pos (line, name) p v t =
     let val name = case name of "" => "unnamed" | name => name
         val arcs = rewrite ["use_text"] name
         (* should we have different files for different line numbers? *
@@ -55,7 +55,7 @@
 		      andalso name = "ML"
 		   then ["empty_Isabelle", "empty" ] else arcs
         val _    = AnnoMaLy.nameNextStream arcs
-    in  smlnj_use_text tune (line, name) p v t  end;
+    in  smlnj_use_text tune str_of_pos (line, name) p v t  end;
 
   fun use_file tune output verbose name =
       let val arcs = rewrite ["use_file"] name