src/HOLCF/Tools/Domain/domain_theorems.ML

 (****************************** induction rules *******************************)
 (******************************************************************************)
 
 fun prove_induction
     (comp_dbind : binding, eqs : eq list)
+    (constr_infos : Domain_Constructors.constr_info list)
+    (take_info : Domain_Take_Proofs.take_induct_info)
     (take_rews : thm list)
-    (take_info : Domain_Take_Proofs.take_induct_info)
     (thy : theory) =
 let
   val comp_dname = Sign.full_name thy comp_dbind;
   val dnames = map (fst o fst) eqs;
   val conss  = map  snd        eqs;
   fun dc_take dn = %%:(dn^"_take");
   val x_name = idx_name dnames "x";
   val P_name = idx_name dnames "P";
   val pg = pg' thy;
 
-  local
-    fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
-    fun gts s dn = Global_Theory.get_thms thy (dn ^ "." ^ s);
-  in
-    val axs_rep_iso = map (ga "rep_iso") dnames;
-    val axs_abs_iso = map (ga "abs_iso") dnames;
-    val exhausts = map (ga  "exhaust" ) dnames;
-    val con_rews  = maps (gts "con_rews" ) dnames;
-  end;
+  val iso_infos = map #iso_info constr_infos;
+  val axs_rep_iso = map #rep_inverse iso_infos;
+  val axs_abs_iso = map #abs_inverse iso_infos;
+  val exhausts = map #exhaust constr_infos;
+  val con_rews = maps #con_rews constr_infos;
 
   val {take_consts, ...} = take_info;
   val {take_0_thms, take_Suc_thms, chain_take_thms, ...} = take_info;
   val {lub_take_thms, finite_defs, reach_thms, ...} = take_info;
   val {take_induct_thms, ...} = take_info;

 
 in thy |> snd o Global_Theory.add_thmss
     [((Binding.qualified true "coinduct" comp_dbind, [coind]), [])]
 end; (* let *)
 
+(******************************************************************************)
+(******************************* main function ********************************)
+(******************************************************************************)
+
 fun comp_theorems
     (comp_dbind : binding, eqs : eq list)
     (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
     (take_info : Domain_Take_Proofs.take_induct_info)
     (constr_infos : Domain_Constructors.constr_info list)

 val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss;
 
 (* prove induction rules, unless definition is indirect recursive *)
 val thy =
     if is_indirect then thy else
-    prove_induction (comp_dbind, eqs) take_rews take_info thy;
+    prove_induction (comp_dbind, eqs) constr_infos take_info take_rews thy;
 
 val thy =
     if is_indirect then thy else
     prove_coinduction (comp_dbind, eqs) take_rews take_lemma_thms thy;