# HG changeset patch
# User wenzelm
# Date 1457040298 -3600
# Node ID 77a5f21c449b0a18d4de8a80bf6d11e6ebc9562b
# Parent  13d6948e4b12b1817baef6b0b39eb86c9c5d4f7d
obsolete;

diff -r 13d6948e4b12 -r 77a5f21c449b src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Thu Mar 03 22:16:52 2016 +0100
+++ b/src/Pure/ML/ml_name_space.ML	Thu Mar 03 22:24:58 2016 +0100
@@ -15,9 +15,7 @@
   type valueVal = Values.value;
   fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
-  val initial_val =
-    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
-      (#allVal global ());
+  val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
 
   type typeVal = TypeConstrs.typeConstr;
   fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);