--- a/src/HOL/ex/CodeEmbed.thy Wed Dec 27 19:10:00 2006 +0100
+++ b/src/HOL/ex/CodeEmbed.thy Wed Dec 27 19:10:03 2006 +0100
@@ -8,9 +8,6 @@
imports Main MLString
begin
-section {* Embedding (a subset of) the Pure term algebra in HOL *}
-
-
subsection {* Definitions *}
types vname = ml_string;