--- 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