# HG changeset patch
# User huffman
# Date 1287092525 25200
# Node ID bf85fef3cce423738b57ee1b055c429ff6b4ca23
# Parent  575d3aa1f3c5d597f3d5289c1133961ee0af7ac8
avoid using Global_Theory.get_thm

diff -r 575d3aa1f3c5 -r bf85fef3cce4 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:46:27 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 14:42:05 2010 -0700
@@ -162,8 +162,9 @@
 
 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;
@@ -174,15 +175,11 @@
   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;
@@ -505,6 +502,10 @@
     [((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)
@@ -545,7 +546,7 @@
 (* 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