# HG changeset patch
# User sultana
# Date 1335273184 -3600
# Node ID 503efdb07566512bceb618b51a6b8c2686729226
# Parent  39c5a1a80accc0d88bec9946a9ad283a5a83ebc7# Parent  6ee015f6ea4b225960d2bd4b395c6af06e746ee6
merged

diff -r 39c5a1a80acc -r 503efdb07566 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Apr 24 14:06:38 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Apr 24 14:13:04 2012 +0100
@@ -285,7 +285,7 @@
   )
 
 fun str_of_pos (pos, triv) =
-  str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^
+  str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^
   (if triv then "[T]" else "")
 
 fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
diff -r 39c5a1a80acc -r 503efdb07566 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Apr 24 14:06:38 2012 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Apr 24 14:13:04 2012 +0100
@@ -108,10 +108,13 @@
 my @lines = <OLD_FILE>;
 close(OLD_FILE);
 
+my $setup_import =
+  substr("\"$output_path\/$setup_thy_name\"" . (" " x 1000), 0, 1000);
+
 my $thy_text = join("", @lines);
 my $old_len = length($thy_text);
 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
-$thy_text =~ s/(imports)(\s+)/$1 "$output_path\/$setup_thy_name"$2/g;
+$thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g;
 die "No 'imports' found" if length($thy_text) == $old_len;
 
 open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";