src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 32729 1441cf4ddc1a
parent 32124 954321008785
child 32905 5e46c6704cee
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Sep 28 10:51:12 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Sep 28 14:48:30 2009 +0200
     1.3 @@ -20,7 +20,7 @@
     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 -      info Symtab.table -> thm list list -> thm list list ->
     1.8 +      (string -> thm list) -> thm list list -> thm list list ->
     1.9          simpset -> thm -> theory -> (string list * thm list) * theory
    1.10    val prove_case_thms : config -> string list ->
    1.11      descr list -> (string * sort) list ->
    1.12 @@ -88,7 +88,7 @@
    1.13  (*************************** primrec combinators ******************************)
    1.14  
    1.15  fun prove_primrec_thms (config : config) new_type_names descr sorts
    1.16 -    (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    1.17 +    injects_of constr_inject dist_rewrites dist_ss induct thy =
    1.18    let
    1.19      val _ = message config "Constructing primrec combinators ...";
    1.20  
    1.21 @@ -174,11 +174,11 @@
    1.22  
    1.23          val inject = map (fn r => r RS iffD1)
    1.24            (if i < length newTs then List.nth (constr_inject, i)
    1.25 -            else #inject (the (Symtab.lookup dt_info tname)));
    1.26 +            else injects_of tname);
    1.27  
    1.28          fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
    1.29            let
    1.30 -            val k = length (List.filter is_rec_type cargs)
    1.31 +            val k = length (filter is_rec_type cargs)
    1.32  
    1.33            in (EVERY [DETERM tac,
    1.34                  REPEAT (etac ex1E 1), rtac ex1I 1,