src/Pure/ROOT
changeset 61925 ab52f183f020
parent 61794 4c232a2ddeab
child 61926 17ba31a2303b
--- a/src/Pure/ROOT	Wed Dec 23 21:15:26 2015 +0100
+++ b/src/Pure/ROOT	Wed Dec 23 23:09:13 2015 +0100
@@ -3,83 +3,83 @@
 session RAW =
   theories
   files
-    "General/exn.ML"
-    "ML-Systems/compiler_polyml.ML"
-    "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/ml_compiler_parameters.ML"
-    "ML-Systems/ml_compiler_parameters_polyml-5.6.ML"
-    "ML-Systems/ml_debugger.ML"
-    "ML-Systems/ml_debugger_polyml-5.6.ML"
-    "ML-Systems/ml_name_space.ML"
-    "ML-Systems/ml_name_space_polyml-5.6.ML"
-    "ML-Systems/ml_name_space_polyml.ML"
-    "ML-Systems/ml_parse_tree.ML"
-    "ML-Systems/ml_parse_tree_polyml-5.6.ML"
-    "ML-Systems/ml_positions.ML"
-    "ML-Systems/ml_pretty.ML"
-    "ML-Systems/ml_profiling_polyml-5.6.ML"
-    "ML-Systems/ml_profiling_polyml.ML"
-    "ML-Systems/ml_stack_dummy.ML"
-    "ML-Systems/ml_stack_polyml-5.6.ML"
-    "ML-Systems/ml_system.ML"
-    "ML-Systems/multithreading.ML"
-    "ML-Systems/multithreading_polyml.ML"
-    "ML-Systems/overloading_smlnj.ML"
-    "ML-Systems/polyml-5.5.2.ML"
-    "ML-Systems/polyml-5.6.ML"
-    "ML-Systems/polyml-5.6.ML"
-    "ML-Systems/polyml.ML"
-    "ML-Systems/pp_dummy.ML"
-    "ML-Systems/proper_int.ML"
-    "ML-Systems/share_common_data_polyml-5.3.0.ML"
-    "ML-Systems/single_assignment.ML"
-    "ML-Systems/single_assignment_polyml.ML"
-    "ML-Systems/smlnj.ML"
-    "ML-Systems/thread_dummy.ML"
-    "ML-Systems/universal.ML"
-    "ML-Systems/unsynchronized.ML"
-    "ML-Systems/use_context.ML"
-    "ML-Systems/windows_path.ML"
+    "RAW/compiler_polyml.ML"
+    "RAW/exn.ML"
+    "RAW/exn_trace_polyml-5.5.1.ML"
+    "RAW/ml_compiler_parameters.ML"
+    "RAW/ml_compiler_parameters_polyml-5.6.ML"
+    "RAW/ml_debugger.ML"
+    "RAW/ml_debugger_polyml-5.6.ML"
+    "RAW/ml_name_space.ML"
+    "RAW/ml_name_space_polyml-5.6.ML"
+    "RAW/ml_name_space_polyml.ML"
+    "RAW/ml_parse_tree.ML"
+    "RAW/ml_parse_tree_polyml-5.6.ML"
+    "RAW/ml_positions.ML"
+    "RAW/ml_pretty.ML"
+    "RAW/ml_profiling_polyml-5.6.ML"
+    "RAW/ml_profiling_polyml.ML"
+    "RAW/ml_stack_dummy.ML"
+    "RAW/ml_stack_polyml-5.6.ML"
+    "RAW/ml_system.ML"
+    "RAW/multithreading.ML"
+    "RAW/multithreading_polyml.ML"
+    "RAW/overloading_smlnj.ML"
+    "RAW/polyml-5.5.2.ML"
+    "RAW/polyml-5.6.ML"
+    "RAW/polyml-5.6.ML"
+    "RAW/polyml.ML"
+    "RAW/pp_dummy.ML"
+    "RAW/proper_int.ML"
+    "RAW/share_common_data_polyml-5.3.0.ML"
+    "RAW/single_assignment.ML"
+    "RAW/single_assignment_polyml.ML"
+    "RAW/smlnj.ML"
+    "RAW/thread_dummy.ML"
+    "RAW/universal.ML"
+    "RAW/unsynchronized.ML"
+    "RAW/use_context.ML"
+    "RAW/windows_path.ML"
 
 session Pure =
   global_theories Pure
   files
-    "General/exn.ML"
-    "ML-Systems/compiler_polyml.ML"
-    "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/ml_compiler_parameters.ML"
-    "ML-Systems/ml_compiler_parameters_polyml-5.6.ML"
-    "ML-Systems/ml_debugger.ML"
-    "ML-Systems/ml_debugger_polyml-5.6.ML"
-    "ML-Systems/ml_name_space.ML"
-    "ML-Systems/ml_name_space_polyml-5.6.ML"
-    "ML-Systems/ml_name_space_polyml.ML"
-    "ML-Systems/ml_parse_tree.ML"
-    "ML-Systems/ml_parse_tree_polyml-5.6.ML"
-    "ML-Systems/ml_positions.ML"
-    "ML-Systems/ml_pretty.ML"
-    "ML-Systems/ml_profiling_polyml-5.6.ML"
-    "ML-Systems/ml_profiling_polyml.ML"
-    "ML-Systems/ml_stack_dummy.ML"
-    "ML-Systems/ml_stack_polyml-5.6.ML"
-    "ML-Systems/ml_system.ML"
-    "ML-Systems/multithreading.ML"
-    "ML-Systems/multithreading_polyml.ML"
-    "ML-Systems/overloading_smlnj.ML"
-    "ML-Systems/polyml-5.5.2.ML"
-    "ML-Systems/polyml-5.6.ML"
-    "ML-Systems/polyml.ML"
-    "ML-Systems/pp_dummy.ML"
-    "ML-Systems/proper_int.ML"
-    "ML-Systems/share_common_data_polyml-5.3.0.ML"
-    "ML-Systems/single_assignment.ML"
-    "ML-Systems/single_assignment_polyml.ML"
-    "ML-Systems/smlnj.ML"
-    "ML-Systems/thread_dummy.ML"
-    "ML-Systems/universal.ML"
-    "ML-Systems/unsynchronized.ML"
-    "ML-Systems/use_context.ML"
-    "ML-Systems/windows_path.ML"
+    "RAW/compiler_polyml.ML"
+    "RAW/exn.ML"
+    "RAW/exn_trace_polyml-5.5.1.ML"
+    "RAW/ml_compiler_parameters.ML"
+    "RAW/ml_compiler_parameters_polyml-5.6.ML"
+    "RAW/ml_debugger.ML"
+    "RAW/ml_debugger_polyml-5.6.ML"
+    "RAW/ml_name_space.ML"
+    "RAW/ml_name_space_polyml-5.6.ML"
+    "RAW/ml_name_space_polyml.ML"
+    "RAW/ml_parse_tree.ML"
+    "RAW/ml_parse_tree_polyml-5.6.ML"
+    "RAW/ml_positions.ML"
+    "RAW/ml_pretty.ML"
+    "RAW/ml_profiling_polyml-5.6.ML"
+    "RAW/ml_profiling_polyml.ML"
+    "RAW/ml_stack_dummy.ML"
+    "RAW/ml_stack_polyml-5.6.ML"
+    "RAW/ml_system.ML"
+    "RAW/multithreading.ML"
+    "RAW/multithreading_polyml.ML"
+    "RAW/overloading_smlnj.ML"
+    "RAW/polyml-5.5.2.ML"
+    "RAW/polyml-5.6.ML"
+    "RAW/polyml.ML"
+    "RAW/pp_dummy.ML"
+    "RAW/proper_int.ML"
+    "RAW/share_common_data_polyml-5.3.0.ML"
+    "RAW/single_assignment.ML"
+    "RAW/single_assignment_polyml.ML"
+    "RAW/smlnj.ML"
+    "RAW/thread_dummy.ML"
+    "RAW/universal.ML"
+    "RAW/unsynchronized.ML"
+    "RAW/use_context.ML"
+    "RAW/windows_path.ML"
 
     "Concurrent/bash.ML"
     "Concurrent/bash_sequential.ML"