--- 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;