# HG changeset patch
# User wenzelm
# Date 1169298550 -3600
# Node ID 025dfa637f783a145c5507f3d64aa9d8bc05869c
# Parent  420b7b102acc51f1c3ccf7b622e2bd28c98638e3
added @{claset};

diff -r 420b7b102acc -r 025dfa637f78 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Fri Jan 19 22:31:17 2007 +0100
+++ b/src/FOL/cladata.ML	Sat Jan 20 14:09:10 2007 +0100
@@ -21,6 +21,8 @@
 structure Cla = ClassicalFun(Classical_Data);
 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
 
+ML_Context.value_antiq "claset"
+  (Scan.succeed ("claset", "Cla.local_claset_of (ML_Context.the_local_context ())"));
 
 
 (*Propositional rules*)