src/Pure/ROOT
changeset 62501 98fa1f9a292f
parent 62498 5dfcc9697f29
child 62504 f14f17e656a6
--- a/src/Pure/ROOT	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/ROOT	Thu Mar 03 11:12:02 2016 +0100
@@ -3,65 +3,39 @@
 session RAW =
   theories
   files
-    "RAW/ROOT_polyml-5.6.ML"
     "RAW/ROOT_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace.ML"
-    "RAW/exn_trace_raw.ML"
     "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler0.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_heap.ML"
-    "RAW/ml_heap_polyml-5.3.0.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_name_space.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_profiling.ML"
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
     "RAW/secure.ML"
-    "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
 
 session Pure =
   global_theories Pure
   files
-    "RAW/ROOT_polyml-5.6.ML"
     "RAW/ROOT_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace.ML"
-    "RAW/exn_trace_raw.ML"
     "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler0.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_heap.ML"
-    "RAW/ml_heap_polyml-5.3.0.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_name_space.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_profiling.ML"
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
     "RAW/secure.ML"
-    "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
 
     "Concurrent/bash.ML"