# HG changeset patch
# User haftmann
# Date 1276165707 -7200
# Node ID 92a75e6d938b649bad14b44e7cee96fa3df02476
# Parent  842fff4c35ef2515da18be8c28b9c27eba163495# Parent  6ff1fce8e156d1591e1e685df31a4c91063e83a2
merged

diff -r 6ff1fce8e156 -r 92a75e6d938b src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Jun 10 12:26:07 2010 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Jun 10 12:28:27 2010 +0200
@@ -63,10 +63,10 @@
 begin
 
 setup {* 
-  Config.put_thy Mirabelle.logfile "$log_file" #>
-  Config.put_thy Mirabelle.timeout $timeout #>
-  Config.put_thy Mirabelle.start_line $start_line #>
-  Config.put_thy Mirabelle.end_line $end_line
+  Config.put_global Mirabelle.logfile "$log_file" #>
+  Config.put_global Mirabelle.timeout $timeout #>
+  Config.put_global Mirabelle.start_line $start_line #>
+  Config.put_global Mirabelle.end_line $end_line
 *}
 
 END