1.1 --- a/src/Pure/Isar/code.ML	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -760,7 +760,7 @@
     1.4  end; (*struct*)
     1.5  
     1.6  
     1.7 -(** type-safe interfaces for data depedent on executable code **)
     1.8 +(** type-safe interfaces for data dependent on executable code **)
     1.9  
    1.10  functor Code_Data_Fun(Data: CODE_DATA_ARGS): CODE_DATA =
    1.11  struct
    1.12 @@ -780,4 +780,13 @@
    1.13  
    1.14  end;
    1.15  
    1.16 +(** datastructure to log definitions for preprocessing of the predicate compiler **)
    1.17 +(*
    1.18 +structure Predicate_Compile_Preproc_Const_Defs = Named_Thms
    1.19 +(
    1.20 +  val name = "predicate_compile_preproc_const_def"
    1.21 +  val description =
    1.22 +    "definitions of constants as needed by the preprocessing for the predicate compiler"
    1.23 +)
    1.24 +*)
    1.25  structure Code : CODE = struct open Code; end;