--- 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,
--- 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'";