eliminated pointless check -- command definitions are subject to theory context;

--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -385,8 +385,6 @@
     : (Domain_Take_Proofs.iso_info list
        * Domain_Take_Proofs.take_induct_info) * theory =
   let
-    val _ = Theory.requires thy (Context.theory_name @{theory}) "domain isomorphisms"
-
     (* this theory is used just for parsing *)
     val tmp_thy = thy |>
       Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) =>

--- a/src/HOL/HOLCF/Tools/cpodef.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -140,8 +140,6 @@
 
 fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
   let
-    val _ = Theory.requires thy (Context.theory_name @{theory}) "cpodefs"
-
     (*rhs*)
     val tmp_ctxt =
       Proof_Context.init_global thy

--- a/src/HOL/HOLCF/Tools/domaindef.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -84,8 +84,6 @@
       (thy: theory)
     : (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
   let
-    val _ = Theory.requires thy (Context.theory_name @{theory}) "domaindefs"
-
     (*rhs*)
     val tmp_ctxt =
       Proof_Context.init_global thy

--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -708,8 +708,6 @@
 
 fun gen_add_datatype prep_specs config raw_specs thy =
   let
-    val _ = Theory.requires thy (Context.theory_name @{theory}) "datatype definitions";
-
     val (dts, spec_ctxt) = prep_specs raw_specs thy;
     val ((_, tyvars, _), _) :: _ = dts;
     val string_of_tyvar = Syntax.string_of_typ spec_ctxt o TFree;

--- a/src/HOL/Tools/inductive.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -1007,9 +1007,6 @@
     cnames_syn pnames spec monos lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val _ =
-      Theory.requires thy (Context.theory_name @{theory})
-        (coind_prefix coind ^ "inductive definitions");
 
 
     (* abbrevs *)

--- a/src/HOL/Tools/recdef.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/HOL/Tools/recdef.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -179,12 +179,9 @@
 
 (** add_recdef(_i) **)
 
-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
     val _ = legacy_feature "Old 'recdef' command -- use 'fun' or 'function' instead";
-    val _ = requires_recdef thy;
 
     val name = Sign.intern_const thy raw_name;
     val bname = Long_Name.base_name name;
@@ -230,7 +227,6 @@
     val name = Sign.intern_const thy raw_name;
     val bname = Long_Name.base_name name;
 
-    val _ = requires_recdef thy;
     val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
 
     val congs = eval_thms (Proof_Context.init_global thy) raw_congs;

--- a/src/HOL/Tools/record.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/HOL/Tools/record.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -2262,8 +2262,6 @@
 
 fun add_record (params, binding) raw_parent raw_fields thy =
   let
-    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)
       handle TYPE (msg, _, _) => error msg;

--- a/src/Pure/theory.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/Pure/theory.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -13,7 +13,6 @@
   val nodes_of: theory -> theory list
   val merge: theory * theory -> theory
   val merge_list: theory list -> theory
-  val requires: theory -> string -> string -> unit
   val setup: (theory -> theory) -> unit
   val get_markup: theory -> Markup.T
   val axiom_table: theory -> term Name_Space.table
@@ -51,10 +50,6 @@
 fun merge_list [] = raise THEORY ("Empty merge of theories", [])
   | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
 
-fun requires thy name what =
-  if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
-  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
-
 fun setup f = Context.>> (Context.map_theory f);
 
 

--- a/src/ZF/Tools/datatype_package.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -64,9 +64,6 @@
 
 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 (Context.theory_name @{theory}) "(co)datatype definitions";
-
   val rec_hds = map head_of rec_tms;
 
   val dummy = rec_hds |> forall (fn t => is_Const t orelse

--- a/src/ZF/Tools/inductive_package.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -59,7 +59,6 @@
 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 (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;