--- a/ProgTutorial/FirstSteps.thy	Sat Aug 22 02:56:08 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Aug 25 00:07:37 2009 +0200
@@ -179,7 +179,7 @@
   @{ML_ind  profiling in Toplevel}.)
 *}
 
-(*
+(* FIXME
 ML {* reset Toplevel.debug *}
 
 ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}
@@ -831,4 +831,18 @@
   own document antiquotations. 
 *}
 
+(*
+section {* Do Not Try This At Home! *}
+
+ML {* val my_thms = ref ([]: thm list) *}
+
+attribute_setup my_thm_bad =
+  {* Scan.succeed (Thm.declaration_attribute (fn th => fn ctxt =>
+      (my_thms := th :: ! my_thms; ctxt))) *} "bad attribute"
+
+declare sym [my_thm_bad]
+declare refl [my_thm_bad]
+
+ML "!my_thms"
+*)
 end