avoid using Global_Theory.get_thm
authorhuffman
Thu Oct 14 14:42:05 2010 -0700 (2010-10-14)
changeset 40018bf85fef3cce4
parent 40017 575d3aa1f3c5
child 40019 05cda34d36e7
avoid using Global_Theory.get_thm
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:46:27 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 14:42:05 2010 -0700
     1.3 @@ -162,8 +162,9 @@
     1.4  
     1.5  fun prove_induction
     1.6      (comp_dbind : binding, eqs : eq list)
     1.7 +    (constr_infos : Domain_Constructors.constr_info list)
     1.8 +    (take_info : Domain_Take_Proofs.take_induct_info)
     1.9      (take_rews : thm list)
    1.10 -    (take_info : Domain_Take_Proofs.take_induct_info)
    1.11      (thy : theory) =
    1.12  let
    1.13    val comp_dname = Sign.full_name thy comp_dbind;
    1.14 @@ -174,15 +175,11 @@
    1.15    val P_name = idx_name dnames "P";
    1.16    val pg = pg' thy;
    1.17  
    1.18 -  local
    1.19 -    fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
    1.20 -    fun gts s dn = Global_Theory.get_thms thy (dn ^ "." ^ s);
    1.21 -  in
    1.22 -    val axs_rep_iso = map (ga "rep_iso") dnames;
    1.23 -    val axs_abs_iso = map (ga "abs_iso") dnames;
    1.24 -    val exhausts = map (ga  "exhaust" ) dnames;
    1.25 -    val con_rews  = maps (gts "con_rews" ) dnames;
    1.26 -  end;
    1.27 +  val iso_infos = map #iso_info constr_infos;
    1.28 +  val axs_rep_iso = map #rep_inverse iso_infos;
    1.29 +  val axs_abs_iso = map #abs_inverse iso_infos;
    1.30 +  val exhausts = map #exhaust constr_infos;
    1.31 +  val con_rews = maps #con_rews constr_infos;
    1.32  
    1.33    val {take_consts, ...} = take_info;
    1.34    val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info;
    1.35 @@ -505,6 +502,10 @@
    1.36      [((Binding.qualified true "coinduct" comp_dbind, [coind]), [])]
    1.37  end; (* let *)
    1.38  
    1.39 +(******************************************************************************)
    1.40 +(******************************* main function ********************************)
    1.41 +(******************************************************************************)
    1.42 +
    1.43  fun comp_theorems
    1.44      (comp_dbind : binding, eqs : eq list)
    1.45      (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
    1.46 @@ -545,7 +546,7 @@
    1.47  (* prove induction rules, unless definition is indirect recursive *)
    1.48  val thy =
    1.49      if is_indirect then thy else
    1.50 -    prove_induction (comp_dbind, eqs) take_rews take_info thy;
    1.51 +    prove_induction (comp_dbind, eqs) constr_infos take_info take_rews thy;
    1.52  
    1.53  val thy =
    1.54      if is_indirect then thy else