src/HOL/Tools/inductive_package.ML
changeset 25822 05756950011c
parent 25510 38c15efe603b
child 25978 8ba1eba8d058
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Jan 03 23:01:51 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jan 03 23:17:01 2008 +0100
     1.3 @@ -54,6 +54,7 @@
     1.4    val arities_of: thm -> (string * int) list
     1.5    val params_of: thm -> term list
     1.6    val partition_rules: thm -> thm list -> (string * thm list) list
     1.7 +  val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
     1.8    val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
     1.9    val infer_intro_vars: thm -> int -> thm list -> term list list
    1.10    val setup: theory -> theory
    1.11 @@ -875,10 +876,13 @@
    1.12    concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const #> fst;
    1.13  
    1.14  (* partition introduction rules according to predicate name *)
    1.15 -fun partition_rules induct intros =
    1.16 -  fold_rev (fn r => AList.map_entry op = (pname_of_intr r) (cons r)) intros
    1.17 +fun gen_partition_rules f induct intros =
    1.18 +  fold_rev (fn r => AList.map_entry op = (pname_of_intr (f r)) (cons r)) intros
    1.19      (map (rpair [] o fst) (arities_of induct));
    1.20  
    1.21 +val partition_rules = gen_partition_rules I;
    1.22 +fun partition_rules' induct = gen_partition_rules fst induct;
    1.23 +
    1.24  fun unpartition_rules intros xs =
    1.25    fold_map (fn r => AList.map_entry_yield op = (pname_of_intr r)
    1.26      (fn x :: xs => (x, xs)) #>> the) intros xs |> fst;