src/Pure/RAW/ml_name_space.ML

--- a/src/Pure/RAW/ml_name_space.ML	Thu Mar 03 11:59:03 2016 +0100
+++ b/src/Pure/RAW/ml_name_space.ML	Thu Mar 03 14:03:06 2016 +0100
@@ -15,19 +15,27 @@
   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 ());
 
   type typeVal = TypeConstrs.typeConstr;
   fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
+  val initial_type = #allType global ();
 
   type fixityVal = Infixes.fixity;
   fun displayFix (_: string, x) = Infixes.print x;
+  val initial_fixity = #allFix global ();
 
   type structureVal = Structures.structureVal;
   fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
+  val initial_structure = #allStruct global ();
 
   type signatureVal = Signatures.signatureVal;
   fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
+  val initial_signature = #allSig global ();
 
   type functorVal = Functors.functorVal;
   fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+  val initial_functor = #allFunct global ();
 end;