handling of definitions

--- a/src/HOL/IsaMakefile	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 23 16:20:12 2009 +0200
@@ -6,7 +6,7 @@
 
 default: HOL
 generate: HOL-Generate-HOL HOL-Generate-HOLLight
-images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4
+images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4 HOL-MicroJava
 
 #Note: keep targets sorted (except for HOL-Library and HOL-ex)
 test: \

--- a/src/HOL/ex/RPred.thy	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/ex/RPred.thy	Wed Sep 23 16:20:12 2009 +0200
@@ -14,13 +14,15 @@
 definition return :: "'a => 'a rpred"
   where "return x = Pair (Predicate.single x)"
 
-definition bind :: "'a rpred \<Rightarrow> ('a \<Rightarrow> 'b rpred) \<Rightarrow> 'b rpred" (infixl "\<guillemotright>=" 60)
+definition bind :: "'a rpred \<Rightarrow> ('a \<Rightarrow> 'b rpred) \<Rightarrow> 'b rpred"
+(* (infixl "\<guillemotright>=" 60) *)
   where "bind RP f =
   (\<lambda>s. let (P, s') = RP s;
         (s1, s2) = Random.split_seed s'
     in (Predicate.bind P (%a. fst (f a s1)), s2))"
 
-definition supp :: "'a rpred \<Rightarrow> 'a rpred \<Rightarrow> 'a rpred" (infixl "\<squnion>" 80)
+definition supp :: "'a rpred \<Rightarrow> 'a rpred \<Rightarrow> 'a rpred"
+(* (infixl "\<squnion>" 80) *)
 where
   "supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s'
   in (upper_semilattice_class.sup P1 P2, s''))"
@@ -43,6 +45,8 @@
   where "lift_random g = scomp g (Pair o (Predicate.single o fst))"
 
 definition map_rpred :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)"
-where "map_rpred f P = P \<guillemotright>= (return o f)"
+where "map_rpred f P = bind P (return o f)"
+
+hide (open) const return bind supp 
   
 end
\ No newline at end of file

--- 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;

--- a/src/Pure/Isar/constdefs.ML	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/Pure/Isar/constdefs.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -52,7 +52,7 @@
       thy
       |> Sign.add_consts_i [(b, T, mx)]
       |> PureThy.add_defs false [((name, def), atts)]
-      |-> (fn [thm] => Code.add_default_eqn thm);
+      |-> (fn [thm] => Code.add_default_eqn thm #> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
   in ((c, T), thy') end;
 
 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =

--- 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,7 @@
         (var, ((Binding.suffix_name "_raw" name, []), rhs));
     val ((def_name, [th']), lthy3) = lthy2
       |> LocalTheory.note Thm.definitionK
-        ((name, Predicate_Compile_Preproc_Const_Defs.add :: Code.add_default_eqn_attrib :: atts),
+        ((name, Predicate_Compile_Preproc_Const_Defs.add_attrib :: Code.add_default_eqn_attrib :: atts),
           [prove lthy2 th]);
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;