# HG changeset patch
# User blanchet
# Date 1459516631 -7200
# Node ID 7737e26cd3c6973ce12d160a369bebb0831942ee
# Parent  f0e8ed202ce5fda906aaf48994c223a4c873e390
adapt theory names within the theory

diff -r f0e8ed202ce5 -r 7737e26cd3c6 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Mar 31 21:19:45 2016 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri Apr 01 15:17:11 2016 +0200
@@ -138,6 +138,7 @@
 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/\b$thy_name\./$new_thy_name./g;
 $thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g;
 die "No 'imports' found" if length($thy_text) == $old_len;