src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 32915 a7a97960054b
parent 32906 ac97e8735cc2
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Oct 12 15:26:50 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Oct 13 08:36:39 2009 +0200
     1.3 @@ -20,8 +20,8 @@
     1.4      attribute list -> theory -> thm list * theory
     1.5    val prove_primrec_thms : config -> string list ->
     1.6      descr list -> (string * sort) list ->
     1.7 -      (string -> thm list) -> thm list list -> thm list list ->
     1.8 -        simpset -> thm -> theory -> (string list * thm list) * theory
     1.9 +      (string -> thm list) -> thm list list -> thm list list * thm list list ->
    1.10 +        thm -> theory -> (string list * thm list) * theory
    1.11    val prove_case_thms : config -> string list ->
    1.12      descr list -> (string * sort) list ->
    1.13        string list -> thm list -> theory -> (thm list list * string list) * theory
    1.14 @@ -88,7 +88,7 @@
    1.15  (*************************** primrec combinators ******************************)
    1.16  
    1.17  fun prove_primrec_thms (config : config) new_type_names descr sorts
    1.18 -    injects_of constr_inject dist_rewrites dist_ss induct thy =
    1.19 +    injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
    1.20    let
    1.21      val _ = message config "Constructing primrec combinators ...";
    1.22  
    1.23 @@ -170,7 +170,7 @@
    1.24          val distinct_tac =
    1.25            (if i < length newTs then
    1.26               full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
    1.27 -           else full_simp_tac dist_ss 1);
    1.28 +           else full_simp_tac (HOL_ss addsimps (flat other_dist_rewrites)) 1);
    1.29  
    1.30          val inject = map (fn r => r RS iffD1)
    1.31            (if i < length newTs then nth constr_inject i