changeset 43560 | d1650e3720fd |
parent 42802 | 51d7e74f6899 |
child 43597 | b4a093e755db |
--- a/src/HOL/HOL.thy Mon Jun 27 15:03:55 2011 +0200 +++ b/src/HOL/HOL.thy Mon Jun 27 16:53:31 2011 +0200 @@ -853,9 +853,11 @@ structure Basic_Classical: BASIC_CLASSICAL = Classical; open Basic_Classical; +*} -ML_Antiquote.value "claset" - (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())"); +setup {* + ML_Antiquote.value @{binding claset} + (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())") *} setup Classical.setup