less global theories -- avoid confusion about special cases;

--- a/src/HOL/Probability/ex/Measure_Not_CCC.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -3,7 +3,7 @@
 section \<open>The Category of Measurable Spaces is not Cartesian Closed\<close>
 
 theory Measure_Not_CCC
-  imports Probability
+  imports "HOL-Probability.Probability"
 begin
 
 text \<open>

--- a/src/HOL/ROOT	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/ROOT	Fri Nov 03 13:43:31 2017 +0100
@@ -687,7 +687,7 @@
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
   theories
-    Probability (global)
+    Probability
   document_files "root.tex"
 
 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
@@ -824,7 +824,7 @@
 
 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   theories
-    SPARK (global)
+    SPARK
 
 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   options [spark_prv = false]

--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -4,7 +4,7 @@
 *)
 
 theory Greatest_Common_Divisor
-imports SPARK
+imports "HOL-SPARK.SPARK"
 begin
 
 spark_proof_functions

--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -4,7 +4,7 @@
 *)
 
 theory Longest_Increasing_Subsequence
-imports SPARK
+imports "HOL-SPARK.SPARK"
 begin
 
 text \<open>

--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory RMD_Specification
-imports RMD SPARK
+imports RMD "HOL-SPARK.SPARK"
 begin
 
 (* bit operations *)

--- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -4,7 +4,7 @@
 *)
 
 theory Sqrt
-imports SPARK
+imports "HOL-SPARK.SPARK"
 begin
 
 spark_open "sqrt/isqrt"

--- a/src/HOL/SPARK/Manual/Complex_Types.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Manual/Complex_Types.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -1,5 +1,5 @@
 theory Complex_Types
-imports SPARK
+imports "HOL-SPARK.SPARK"
 begin
 
 datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun

--- a/src/HOL/SPARK/Manual/Proc1.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Manual/Proc1.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -1,5 +1,5 @@
 theory Proc1
-imports SPARK
+imports "HOL-SPARK.SPARK"
 begin
 
 spark_open "loop_invariant/proc1"

--- a/src/HOL/SPARK/Manual/Proc2.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Manual/Proc2.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -1,5 +1,5 @@
 theory Proc2
-imports SPARK
+imports "HOL-SPARK.SPARK"
 begin
 
 spark_open "loop_invariant/proc2"

--- a/src/HOL/SPARK/Manual/Reference.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Manual/Reference.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory Reference
-imports SPARK
+imports "HOL-SPARK.SPARK"
 begin
 
 syntax (my_constrain output)

--- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Thu Nov 02 15:21:35 2017 +0100
+++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Fri Nov 03 13:43:31 2017 +0100
@@ -4,7 +4,7 @@
 *)
 
 theory Simple_Greatest_Common_Divisor
-imports SPARK
+imports "HOL-SPARK.SPARK"
 begin
 
 spark_proof_functions