# HG changeset patch
# User wenzelm
# Date 1395500307 -3600
# Node ID 0fda98dd2c9317cb1c073934a056120b01ccb473
# Parent  1ad01f98dc3eac8ab28d159b3f9d0a71867c5c7c
avoid hard-wired theory names;

diff -r 1ad01f98dc3e -r 0fda98dd2c93 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Mar 22 15:58:27 2014 +0100
@@ -404,7 +404,7 @@
     : (Domain_Take_Proofs.iso_info list
        * Domain_Take_Proofs.take_induct_info) * theory =
   let
-    val _ = Theory.requires thy "Domain" "domain isomorphisms"
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "domain isomorphisms"
 
     (* this theory is used just for parsing *)
     val tmp_thy = thy |>
diff -r 1ad01f98dc3e -r 0fda98dd2c93 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sat Mar 22 15:58:27 2014 +0100
@@ -140,7 +140,7 @@
 
 fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
   let
-    val _ = Theory.requires thy "Cpodef" "cpodefs"
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "cpodefs"
 
     (*rhs*)
     val tmp_ctxt =
diff -r 1ad01f98dc3e -r 0fda98dd2c93 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sat Mar 22 15:58:27 2014 +0100
@@ -84,7 +84,7 @@
       (thy: theory)
     : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
   let
-    val _ = Theory.requires thy "Domain" "domaindefs"
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "domaindefs"
 
     (*rhs*)
     val tmp_ctxt =
diff -r 1ad01f98dc3e -r 0fda98dd2c93 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 15:58:27 2014 +0100
@@ -707,7 +707,7 @@
 
 fun gen_add_datatype prep_specs config raw_specs thy =
   let
-    val _ = Theory.requires thy "Datatype" "datatype definitions";
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "datatype definitions";
 
     val (dts, spec_ctxt) = prep_specs raw_specs thy;
     val ((_, tyvars, _), _) :: _ = dts;
diff -r 1ad01f98dc3e -r 0fda98dd2c93 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Sat Mar 22 15:58:27 2014 +0100
@@ -1000,7 +1000,9 @@
     cnames_syn pnames spec monos lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
+    val _ =
+      Theory.requires thy (Context.theory_name @{theory})
+        (coind_prefix coind ^ "inductive definitions");
 
 
     (* abbrevs *)
diff -r 1ad01f98dc3e -r 0fda98dd2c93 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Tools/recdef.ML	Sat Mar 22 15:58:27 2014 +0100
@@ -180,7 +180,7 @@
 
 (** add_recdef(_i) **)
 
-fun requires_recdef thy = Theory.requires thy "Old_Recdef" "recursive functions";
+fun requires_recdef thy = Theory.requires thy (Context.theory_name @{theory}) "recursive functions";
 
 fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
   let
diff -r 1ad01f98dc3e -r 0fda98dd2c93 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 22 15:58:27 2014 +0100
@@ -2245,7 +2245,7 @@
 
 fun add_record (params, binding) raw_parent raw_fields thy =
   let
-    val _ = Theory.requires thy "Record" "record definitions";
+    val _ = Theory.requires thy (Context.theory_name @{theory}) "record definitions";
 
     val ctxt = Proof_Context.init_global thy;
     fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
diff -r 1ad01f98dc3e -r 0fda98dd2c93 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sat Mar 22 15:58:27 2014 +0100
@@ -65,7 +65,7 @@
 fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
  let
   val dummy = (*has essential ancestors?*)
-    Theory.requires thy "Datatype_ZF" "(co)datatype definitions";
+    Theory.requires thy (Context.theory_name @{theory}) "(co)datatype definitions";
 
   val rec_hds = map head_of rec_tms;
 
diff -r 1ad01f98dc3e -r 0fda98dd2c93 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 22 15:58:27 2014 +0100
@@ -59,7 +59,7 @@
 fun add_inductive_i verbose (rec_tms, dom_sum)
   raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
 let
-  val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
+  val _ = Theory.requires thy (Context.theory_name @{theory}) "(co)inductive definitions";
   val ctxt = Proof_Context.init_global thy;
 
   val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;