# HG changeset patch
# User berghofe
# Date 1199398621 -3600
# Node ID 05756950011c5e184472d14ff637a0b997af9aa2
# Parent  2e565f8275f5cc902578e1aef26d1a616817d0ad
Added function partition_rules'.

diff -r 2e565f8275f5 -r 05756950011c src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Jan 03 23:01:51 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Jan 03 23:17:01 2008 +0100
@@ -54,6 +54,7 @@
   val arities_of: thm -> (string * int) list
   val params_of: thm -> term list
   val partition_rules: thm -> thm list -> (string * thm list) list
+  val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
   val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
   val infer_intro_vars: thm -> int -> thm list -> term list list
   val setup: theory -> theory
@@ -875,10 +876,13 @@
   concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const #> fst;
 
 (* partition introduction rules according to predicate name *)
-fun partition_rules induct intros =
-  fold_rev (fn r => AList.map_entry op = (pname_of_intr r) (cons r)) intros
+fun gen_partition_rules f induct intros =
+  fold_rev (fn r => AList.map_entry op = (pname_of_intr (f r)) (cons r)) intros
     (map (rpair [] o fst) (arities_of induct));
 
+val partition_rules = gen_partition_rules I;
+fun partition_rules' induct = gen_partition_rules fst induct;
+
 fun unpartition_rules intros xs =
   fold_map (fn r => AList.map_entry_yield op = (pname_of_intr r)
     (fn x :: xs => (x, xs)) #>> the) intros xs |> fst;