# HG changeset patch
# User boehmes
# Date 1251095620 -7200
# Node ID 9692b0714295d55a4d4073c7631a89a42bce864a
# Parent  e8feef03a93f520521deb7729e974096ea124fcc
do not introduce additional newlines

diff -r e8feef03a93f -r 9692b0714295 src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Sat Aug 22 23:22:17 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 24 08:33:40 2009 +0200
@@ -99,7 +99,8 @@
 
 my $thy_text = join("", @lines);
 my $old_len = length($thy_text);
-$thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$setup_thy_name" /gm;
+$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
+$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$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'";