diff -r e450fa467e3f -r 2b7c08d90e2e ProgTutorial/FirstSteps.thy --- 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