--- a/src/FOL/FOL.thy Mon Jun 27 15:03:55 2011 +0200
+++ b/src/FOL/FOL.thy Mon Jun 27 16:53:31 2011 +0200
@@ -177,12 +177,15 @@
val hyp_subst_tacs = [hyp_subst_tac]
);
-ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
-
structure Basic_Classical: BASIC_CLASSICAL = Cla;
open Basic_Classical;
*}
+setup {*
+ ML_Antiquote.value @{binding claset}
+ (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())")
+*}
+
setup Cla.setup
(*Propositional rules*)