# HG changeset patch
# User krauss
# Date 1300714630 -3600
# Node ID 1571fde21911a172e7da86a72f5538f1a659334d
# Parent  a14e9cf805e00058a5911d881ccaed5241163787
eliminated unnecessary generated ROOT.ML

diff -r a14e9cf805e0 -r 1571fde21911 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 14:25:59 2011 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 14:37:10 2011 +0100
@@ -116,11 +116,6 @@
 print NEW_FILE $thy_text;
 close(NEW_FILE);
 
-my $root_file = "$output_path/ROOT_$thy_name.ML";
-open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
-print ROOT_FILE "use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n";
-close(ROOT_FILE);
-
 
 # run isabelle
 
@@ -139,14 +134,13 @@
 print "Mirabelle: $thy_file\n" if ($quiet ne "");
 
 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
-  "-e 'use \"$root_file\";' -q $mirabelle_logic" . $quiet;
+  "-e 'use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
 
 print "Finished:  $thy_file\n" if ($quiet ne "");
 
 
 # cleanup
 
-unlink $root_file;
 unlink $setup_file;
 unlink $new_thy_file;