moved global ML bindings to global place;

--- a/src/HOL/Main.thy	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/Main.thy	Wed Sep 17 21:27:14 2008 +0200
@@ -8,8 +8,6 @@
 imports Plain Code_Eval Map Nat_Int_Bij Recdef
 begin
 
-ML {* val HOL_proofs = ! Proofterm.proofs *}
-
 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
 end

--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Sep 17 21:27:14 2008 +0200
@@ -73,10 +73,6 @@
 
 val Eindhoven_ss =
   @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
-
-(*check if user has pmu installed*)
-fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
-fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
 *}
 
 end

--- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed Sep 17 21:27:14 2008 +0200
@@ -236,11 +236,6 @@
         full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
         move_mus i, call_mucke_tac i,atac i,
         REPEAT (rtac refl i)] state);
-
-(*check if user has mucke installed*)
-fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
-fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
-
 *}
 
 end

--- a/src/HOL/Modelcheck/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/Modelcheck/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
@@ -10,6 +10,10 @@
 
 (* Einhoven model checker *)
 
+(*check if user has pmu installed*)
+fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
+fun if_eindhoven_enabled f x = if eindhoven_enabled () then f x else ();
+
 time_use_thy "EindhovenSyn";
 if_eindhoven_enabled time_use_thy "EindhovenExample";
 
@@ -18,5 +22,9 @@
 
 time_use_thy "MuckeSyn";
 
+(*check if user has mucke installed*)
+fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
+fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
+
 if_mucke_enabled time_use_thy "MuckeExample1";
 if_mucke_enabled time_use_thy "MuckeExample2";

--- a/src/HOL/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
@@ -5,3 +5,6 @@
 *)
 
 use_thy "Complex/Complex_Main";
+
+val HOL_proofs = ! Proofterm.proofs;
+

--- a/src/HOL/ex/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
@@ -72,6 +72,11 @@
 time_use_thy "Reflection";
 
 time_use_thy "SVC_Oracle";
+
+(*check if user has SVC installed*)
+fun svc_enabled () = getenv "SVC_HOME" <> "";
+fun if_svc_enabled f x = if svc_enabled () then f x else ();
+
 if_svc_enabled time_use_thy "svc_test";
 
 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)

--- a/src/HOL/ex/SVC_Oracle.thy	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Wed Sep 17 21:27:14 2008 +0200
@@ -116,11 +116,6 @@
     val th = svc_oracle (Thm.theory_of_thm st) abs_goal
    in compose_tac (false, th, 0) i st end
    handle TERM _ => no_tac st;
-
-
-(*check if user has SVC installed*)
-fun svc_enabled () = getenv "SVC_HOME" <> "";
-fun if_svc_enabled f x = if svc_enabled () then f x else ();
 *}
 
 end

--- a/src/HOLCF/IOA/Modelcheck/ROOT.ML	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML	Wed Sep 17 21:27:14 2008 +0200
@@ -7,6 +7,10 @@
 
 with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle";
 
+(*check if user has mucke installed*)
+fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
+fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
+
 (*examples*)
 if_mucke_enabled time_use_thy "Cockpit";
 if_mucke_enabled time_use_thy "Ring3";