# HG changeset patch # User wenzelm # Date 1415394951 -3600 # Node ID 7fbe4436952d355d267755e981fd49a48bda17e7 # Parent dcad9bad43e7654c68df404f27923ce0b63c44af eliminated pointless check -- command definitions are subject to theory context; diff -r dcad9bad43e7 -r 7fbe4436952d src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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, _, _) => diff -r dcad9bad43e7 -r 7fbe4436952d src/HOL/HOLCF/Tools/cpodef.ML --- 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 diff -r dcad9bad43e7 -r 7fbe4436952d src/HOL/HOLCF/Tools/domaindef.ML --- 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 diff -r dcad9bad43e7 -r 7fbe4436952d src/HOL/Tools/Old_Datatype/old_datatype.ML --- 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; diff -r dcad9bad43e7 -r 7fbe4436952d src/HOL/Tools/inductive.ML --- 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 *) diff -r dcad9bad43e7 -r 7fbe4436952d src/HOL/Tools/recdef.ML --- 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; diff -r dcad9bad43e7 -r 7fbe4436952d src/HOL/Tools/record.ML --- 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; diff -r dcad9bad43e7 -r 7fbe4436952d src/Pure/theory.ML --- 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); diff -r dcad9bad43e7 -r 7fbe4436952d src/ZF/Tools/datatype_package.ML --- 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 diff -r dcad9bad43e7 -r 7fbe4436952d src/ZF/Tools/inductive_package.ML --- 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;