src/HOL/ex/Cartouche_Examples.thy

--- a/src/HOL/ex/Cartouche_Examples.thy	Thu Apr 07 20:54:20 2016 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Apr 07 21:27:17 2016 +0200
@@ -272,12 +272,4 @@
     if Symbol.is_digit s then Position.report pos Markup.ML_numeral else ());
 \<close>
 
-text \<open>Nested ML evaluation:\<close>
-ML \<open>
-  ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
-  ML \<open>val b = @{thm sym}\<close>;
-  val c = @{thm trans}
-  val thms = [a, b, c];
-\<close>
-
 end