renaming code_pred_intros to code_pred_intro
* * *
adopted alternative definitions for the predicate compiler to new attribute name

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 12 09:11:31 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Nov 12 09:11:36 2009 +0100
@@ -36,7 +36,7 @@
   val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
   val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
     option Unsynchronized.ref
-  val code_pred_intros_attrib : attribute
+  val code_pred_intro_attrib : attribute
   (* used by Quickcheck_Generator *) 
   (* temporary for testing of the compilation *)
   datatype compilation_funs = CompilationFuns of {
@@ -2418,19 +2418,16 @@
 
 fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
 
-val code_pred_intros_attrib = attrib add_intro;
+val code_pred_intro_attrib = attrib add_intro;
 
 
 (*FIXME
 - Naming of auxiliary rules necessary?
-- add default code equations P x y z = P_i_i_i x y z
 *)
 
 val setup = PredData.put (Graph.empty) #>
-  Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
+  Attrib.setup @{binding code_pred_intro} (Scan.succeed (attrib add_intro))
     "adding alternative introduction rules for code generation of inductive predicates"
-  (*FIXME name discrepancy in attribs and ML code*)
-  (*FIXME intros should be better named intro*)
 
 (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
 fun generic_code_pred prep_const options raw_const lthy =

--- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy	Thu Nov 12 09:11:31 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy	Thu Nov 12 09:11:36 2009 +0100
@@ -12,12 +12,12 @@
  
 subsection {* Alternative rules for set *}
 
-lemma set_ConsI1 [code_pred_intros]:
+lemma set_ConsI1 [code_pred_intro]:
   "set (x # xs) x"
 unfolding mem_def[symmetric, of _ x]
 by auto
 
-lemma set_ConsI2 [code_pred_intros]:
+lemma set_ConsI2 [code_pred_intro]:
   "set xs x ==> set (x' # xs) x" 
 unfolding mem_def[symmetric, of _ x]
 by auto
@@ -37,10 +37,10 @@
 
 subsection {* Alternative rules for list_all2 *}
 
-lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []"
+lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
 by auto
 
-lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
+lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
 by auto
 
 code_pred list_all2

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 12 09:11:31 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Thu Nov 12 09:11:36 2009 +0100
@@ -103,11 +103,11 @@
 where
   "(x = D) \<or> (x = E) ==> is_D_or_E x"
 
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
   "is_D_or_E D"
 by (auto intro: is_D_or_E.intros)
 
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
   "is_D_or_E E"
 by (auto intro: is_D_or_E.intros)
 
@@ -134,11 +134,11 @@
 where
   "x = F \<or> x = G ==> is_F_or_G x"
 
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
   "is_F_or_G F"
 by (auto intro: is_F_or_G.intros)
 
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
   "is_F_or_G G"
 by (auto intro: is_F_or_G.intros)
 
@@ -308,7 +308,7 @@
 lemma append2_Nil: "append2 [] (xs::'b list) xs"
   by (simp add: append2.intros(1))
 
-lemmas [code_pred_intros] = append2_Nil append2.intros(2)
+lemmas [code_pred_intro] = append2_Nil append2.intros(2)
 
 code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool,
   i => o => i => bool, i => i => i => bool) append2
@@ -469,7 +469,7 @@
 
 thm tupled_partition.equation
 
-lemma [code_pred_intros]:
+lemma [code_pred_intro]:
   "r a b \<Longrightarrow> tranclp r a b"
   "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
   by auto
@@ -965,9 +965,9 @@
 | objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
 | plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
 
-(* TODO: breaks if code_pred_intros is used? *)
+(* TODO: breaks if code_pred_intro is used? *)
 (*
-lemmas [code_pred_intros] = irconst objaddr plus
+lemmas [code_pred_intro] = irconst objaddr plus
 *)
 thm eval_var.cases