# HG changeset patch
# User bulwahn
# Date 1253715612 -7200
# Node ID f4d179d91af25016ffefa525f9023646dcbf663c
# Parent  e3aab585531da5fbae165463e370c505895dfc16
experimenting to add some useful interface for definitions

diff -r e3aab585531d -r f4d179d91af2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
@@ -2023,13 +2023,7 @@
 
 subsection {* Preprocessing for the predicate compiler *}
 
-ML {*
-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 "
-)
-*}
+setup {* Predicate_Compile_Preproc_Const_Defs.setup *}
 
 subsection {* Nitpick setup *}
 
diff -r e3aab585531d -r f4d179d91af2 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
@@ -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;
diff -r e3aab585531d -r f4d179d91af2 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -209,7 +209,8 @@
         (var, ((Binding.suffix_name "_raw" name, []), rhs));
     val ((def_name, [th']), lthy3) = lthy2
       |> LocalTheory.note Thm.definitionK
-        ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
+        ((name, Predicate_Compile_Preproc_Const_Defs.add :: Code.add_default_eqn_attrib :: atts),
+          [prove lthy2 th]);
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
     val _ =