src/Pure/Isar/code.ML

--- a/src/Pure/Isar/code.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/Pure/Isar/code.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -781,12 +781,48 @@
 end;
 
 (** datastructure to log definitions for preprocessing of the predicate compiler **)
-(*
-structure Predicate_Compile_Preproc_Const_Defs = Named_Thms
+(* obviously a clone of Named_Thms *)
+
+signature PREDICATE_COMPILE_PREPROC_CONST_DEFS =
+sig
+  val get: Proof.context -> thm list
+  val add_thm: thm -> Context.generic -> Context.generic
+  val del_thm: thm -> Context.generic -> Context.generic
+  
+  val add_attribute : attribute
+  val del_attribute : attribute
+  
+  val add_attrib : Attrib.src
+  
+  val setup: theory -> theory
+end;
+
+structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS =
+struct
+
+structure Data = GenericDataFun
 (
-  val name = "predicate_compile_preproc_const_def"
-  val description =
-    "definitions of constants as needed by the preprocessing for the predicate compiler"
-)
-*)
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  fun merge _ = Thm.merge_thms;
+);
+
+val get = Data.get o Context.Proof;
+
+val add_thm = Data.map o Thm.add_thm;
+val del_thm = Data.map o Thm.del_thm;
+
+val add_attribute = Thm.declaration_attribute add_thm;
+val del_attribute = Thm.declaration_attribute del_thm;
+
+val add_attrib = Attrib.internal (K add_attribute)
+
+val setup =
+  Attrib.setup (Binding.name "pred_compile_preproc") (Attrib.add_del add_attribute del_attribute)
+    ("declaration of definition for preprocessing of the predicate compiler") #>
+  PureThy.add_thms_dynamic (Binding.name "pred_compile_preproc", Data.get);
+
+end;
+
 structure Code : CODE = struct open Code; end;