src/Doc/Implementation/Proof.thy

 \<close>
 
 text %mlex \<open>The following example shows how to work with fixed term
   and type parameters and with type-inference.\<close>
 
-ML \<open>
+ML_val \<open>
   (*static compile-time context -- for testing only*)
   val ctxt0 = @{context};
 
   (*locally fixed parameters -- no type assignment yet*)
   val ([x, y], ctxt1) = ctxt0 |> Variable.add_fixes ["x", "y"];

   literally: @{text "x"} is mapped again to @{text "x"}, and
   attempting to fix it again in the subsequent context is an error.
   Alternatively, fixed parameters can be renamed explicitly as
   follows:\<close>
 
-ML \<open>
+ML_val \<open>
   val ctxt0 = @{context};
   val ([x1, x2, x3], ctxt1) =
     ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
 \<close>
 

   derived by building up a context of assumptions first, and exporting
   some local fact afterwards.  We refer to @{theory Pure} equality
   here for testing purposes.
 \<close>
 
-ML \<open>
+ML_val \<open>
   (*static compile-time context -- for testing only*)
   val ctxt0 = @{context};
 
   val ([eq], ctxt1) =
     ctxt0 |> Assumption.add_assumes [@{cprop "x \<equiv> y"}];