# HG changeset patch
# User wenzelm
# Date 878632052 -3600
# Node ID d7c963600bda813580647989615cd2799b4fd407
# Parent  b131edcfeac3c4ffde6518ce0ab51e921aac3d62
fixed set_current_thy pattern;

diff -r b131edcfeac3 -r d7c963600bda lib/scripts/fixclasimp.pl
--- a/lib/scripts/fixclasimp.pl	Tue Nov 04 09:26:15 1997 +0100
+++ b/lib/scripts/fixclasimp.pl	Tue Nov 04 09:27:32 1997 +0100
@@ -13,7 +13,7 @@
 
     $_ = $text;
 
-    s/set_current_thy\s"([^"]*)"/context $1.thy/sg;
+    s/set_current_thy\s*"([^"]*)"/context $1.thy/sg;
 
     s/!\s*simpset/simpset()/sg;
     s/simpset\s*:=/simpset_ref() :=/sg;