--- a/CookBook/Package/simple_inductive_package.ML	Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Wed Mar 11 01:43:28 2009 +0000
@@ -137,24 +137,25 @@
   end)
 (* @end *)
 
+fun introductions_tac defs rules preds i ctxt =
+  EVERY1 [ObjectLogic.rulify_tac,
+          K (rewrite_goals_tac defs),
+          REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
+          subproof1 rules preds i ctxt]
+
+
 (* @chunk intro_rules *) 
-fun INTROS rules parnames preds defs lthy1 = 
+fun introductions rules parnames preds defs lthy1 = 
 let
   val (_, lthy2) = Variable.add_fixes parnames lthy1
 
   fun prove_intro (i, goal) =
     Goal.prove lthy2 [] [] goal
-        (fn {context = ctxt, ...} => 
-           EVERY1
-           [ObjectLogic.rulify_tac,
-            K (rewrite_goals_tac defs),
-            REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
-            subproof1 rules preds i ctxt])
-        |> singleton (ProofContext.export lthy2 lthy1)
+       (fn {context, ...} => introductions_tac defs rules preds i context)
+       |> singleton (ProofContext.export lthy2 lthy1)
 in
   map_index prove_intro rules
 end
-
 (* @end *)
 
 (* @chunk add_inductive_i *)
@@ -163,7 +164,7 @@
   val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params;
   val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds;
   val Tss = map (binder_types o fastype_of) preds';   
-  val (ass,rules) = split_list specs;    
+  val (ass, rules) = split_list specs;  (* FIXME: ass not used? *)  
 
   val prednames = map (fst o fst) preds
   val syns = map snd preds
@@ -173,7 +174,7 @@
       
   val inducts = inductions rules defs parnames preds' Tss lthy1 	
   
-  val intros = INTROS rules parnames preds' defs lthy1
+  val intros = introductions rules parnames preds' defs lthy1
 
   val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds);
   val case_names = map (Binding.name_of o fst o fst) specs