src/Pure/Isar/code.ML
changeset 32661 f4d179d91af2
parent 32640 ba6531df2c64
child 32662 2faf1148c062
--- 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
@@ -760,7 +760,7 @@
 end; (*struct*)
 
 
-(** type-safe interfaces for data depedent on executable code **)
+(** type-safe interfaces for data dependent on executable code **)
 
 functor Code_Data_Fun(Data: CODE_DATA_ARGS): CODE_DATA =
 struct
@@ -780,4 +780,13 @@
 
 end;
 
+(** datastructure to log definitions for preprocessing of the predicate compiler **)
+(*
+structure Predicate_Compile_Preproc_Const_Defs = Named_Thms
+(
+  val name = "predicate_compile_preproc_const_def"
+  val description =
+    "definitions of constants as needed by the preprocessing for the predicate compiler"
+)
+*)
 structure Code : CODE = struct open Code; end;