| changeset 22127 | 025dfa637f78 |
| parent 21539 | c5cf9243ad62 |
| child 26287 | df8e5362cff9 |
--- 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*)