experimenting to add some useful interface for definitions
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 32661f4d179d91af2
parent 32660 e3aab585531d
child 32662 2faf1148c062
experimenting to add some useful interface for definitions
src/HOL/HOL.thy
src/Pure/Isar/code.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -2023,13 +2023,7 @@
     1.4  
     1.5  subsection {* Preprocessing for the predicate compiler *}
     1.6  
     1.7 -ML {*
     1.8 -structure Predicate_Compile_Preproc_Const_Defs = Named_Thms
     1.9 -(
    1.10 -  val name = "predicate_compile_preproc_const_def"
    1.11 -  val description = "definitions of constants as needed by the preprocessing for the predicate compiler "
    1.12 -)
    1.13 -*}
    1.14 +setup {* Predicate_Compile_Preproc_Const_Defs.setup *}
    1.15  
    1.16  subsection {* Nitpick setup *}
    1.17  
     2.1 --- a/src/Pure/Isar/code.ML	Wed Sep 23 16:20:12 2009 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Wed Sep 23 16:20:12 2009 +0200
     2.3 @@ -760,7 +760,7 @@
     2.4  end; (*struct*)
     2.5  
     2.6  
     2.7 -(** type-safe interfaces for data depedent on executable code **)
     2.8 +(** type-safe interfaces for data dependent on executable code **)
     2.9  
    2.10  functor Code_Data_Fun(Data: CODE_DATA_ARGS): CODE_DATA =
    2.11  struct
    2.12 @@ -780,4 +780,13 @@
    2.13  
    2.14  end;
    2.15  
    2.16 +(** datastructure to log definitions for preprocessing of the predicate compiler **)
    2.17 +(*
    2.18 +structure Predicate_Compile_Preproc_Const_Defs = Named_Thms
    2.19 +(
    2.20 +  val name = "predicate_compile_preproc_const_def"
    2.21 +  val description =
    2.22 +    "definitions of constants as needed by the preprocessing for the predicate compiler"
    2.23 +)
    2.24 +*)
    2.25  structure Code : CODE = struct open Code; end;
     3.1 --- a/src/Pure/Isar/specification.ML	Wed Sep 23 16:20:12 2009 +0200
     3.2 +++ b/src/Pure/Isar/specification.ML	Wed Sep 23 16:20:12 2009 +0200
     3.3 @@ -209,7 +209,8 @@
     3.4          (var, ((Binding.suffix_name "_raw" name, []), rhs));
     3.5      val ((def_name, [th']), lthy3) = lthy2
     3.6        |> LocalTheory.note Thm.definitionK
     3.7 -        ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
     3.8 +        ((name, Predicate_Compile_Preproc_Const_Defs.add :: Code.add_default_eqn_attrib :: atts),
     3.9 +          [prove lthy2 th]);
    3.10  
    3.11      val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
    3.12      val _ =