src/Doc/Implementation/Prelim.thy

--- a/src/Doc/Implementation/Prelim.thy	Wed Apr 01 22:08:06 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Wed Apr 01 22:40:07 2015 +0200
@@ -501,6 +501,9 @@
   value can be modified within Isar text like this:
 \<close>
 
+experiment
+begin
+
 declare [[show_types = false]]
   -- \<open>declaration within (local) theory context\<close>
 
@@ -516,6 +519,8 @@
     ..
 end
 
+end
+
 text \<open>Configuration options that are not set explicitly hold a
   default value that can depend on the application context.  This
   allows to retrieve the value from another slot within the context,
@@ -720,7 +725,7 @@
 text %mlex \<open>The following simple examples demonstrate how to produce
   fresh names from the initial @{ML Name.context}.\<close>
 
-ML \<open>
+ML_val \<open>
   val list1 = Name.invent Name.context "a" 5;
   @{assert} (list1 = ["a", "b", "c", "d", "e"]);
 
@@ -732,10 +737,10 @@
 text \<open>\medskip The same works relatively to the formal context as
   follows.\<close>
 
-locale ex = fixes a b c :: 'a
+experiment fixes a b c :: 'a
 begin
 
-ML \<open>
+ML_val \<open>
   val names = Variable.names_of @{context};
 
   val list1 = Name.invent names "a" 5;
@@ -1043,7 +1048,7 @@
   concrete binding inlined into the text:
 \<close>
 
-ML \<open>Binding.pos_of @{binding here}\<close>
+ML_val \<open>Binding.pos_of @{binding here}\<close>
 
 text \<open>\medskip That position can be also printed in a message as
   follows:\<close>