--- a/Nominal/Ex3.thy Tue Mar 23 08:45:08 2010 +0100
+++ b/Nominal/Ex3.thy Tue Mar 23 08:46:44 2010 +0100
@@ -2,6 +2,8 @@
imports "Parser"
begin
+(* Example 3, identical to example 1 from Terms.thy *)
+
atom_decl name
ML {* val _ = recursive := false *}