src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 40017 575d3aa1f3c5
parent 40016 2eff1cbc1ccb
child 40018 bf85fef3cce4
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:28:31 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:46:27 2010 -0700
     1.3 @@ -12,7 +12,6 @@
     1.4    val comp_theorems :
     1.5        binding * Domain_Library.eq list ->
     1.6        (binding * (binding * (bool * binding option * typ) list * mixfix) list) list ->
     1.7 -      Domain_Take_Proofs.iso_info list ->
     1.8        Domain_Take_Proofs.take_induct_info ->
     1.9        Domain_Constructors.constr_info list ->
    1.10        theory -> thm list * theory
    1.11 @@ -99,7 +98,6 @@
    1.12  
    1.13  fun take_theorems
    1.14      (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
    1.15 -    (iso_infos : Domain_Take_Proofs.iso_info list)
    1.16      (take_info : Domain_Take_Proofs.take_induct_info)
    1.17      (constr_infos : Domain_Constructors.constr_info list)
    1.18      (thy : theory) : thm list list * theory =
    1.19 @@ -113,7 +111,7 @@
    1.20    val n' = @{const Suc} $ n;
    1.21  
    1.22    local
    1.23 -    val newTs = map #absT iso_infos;
    1.24 +    val newTs = map (#absT o #iso_info) constr_infos;
    1.25      val subs = newTs ~~ map (fn t => t $ n) take_consts;
    1.26      fun is_ID (Const (c, _)) = (c = @{const_name ID})
    1.27        | is_ID _              = false;
    1.28 @@ -124,9 +122,9 @@
    1.29    end
    1.30  
    1.31    fun prove_take_apps
    1.32 -      ((((dbind, spec), iso_info), take_const), constr_info) thy =
    1.33 +      (((dbind, spec), take_const), constr_info) thy =
    1.34      let
    1.35 -      val {con_consts, con_betas, ...} = constr_info;
    1.36 +      val {iso_info, con_consts, con_betas, ...} = constr_info;
    1.37        val {abs_inverse, ...} = iso_info;
    1.38        fun prove_take_app (con_const : term) (bind, args, mx) =
    1.39          let
    1.40 @@ -151,7 +149,7 @@
    1.41      end;
    1.42  in
    1.43    fold_map prove_take_apps
    1.44 -    (specs ~~ iso_infos ~~ take_consts ~~ constr_infos) thy
    1.45 +    (specs ~~ take_consts ~~ constr_infos) thy
    1.46  end;
    1.47  
    1.48  (* ----- general proofs ----------------------------------------------------- *)
    1.49 @@ -510,7 +508,6 @@
    1.50  fun comp_theorems
    1.51      (comp_dbind : binding, eqs : eq list)
    1.52      (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
    1.53 -    (iso_infos : Domain_Take_Proofs.iso_info list)
    1.54      (take_info : Domain_Take_Proofs.take_induct_info)
    1.55      (constr_infos : Domain_Constructors.constr_info list)
    1.56      (thy : theory) =
    1.57 @@ -539,7 +536,7 @@
    1.58  (* theorems about take *)
    1.59  
    1.60  val (take_rewss, thy) =
    1.61 -    take_theorems specs iso_infos take_info constr_infos thy;
    1.62 +    take_theorems specs take_info constr_infos thy;
    1.63  
    1.64  val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;
    1.65