# HG changeset patch
# User wenzelm
# Date 924778239 -7200
# Node ID 48f90bc10cf5cff3ce695d96c597b6eea1eedee6
# Parent  e36581d04eee59c51f4eadace672cb3e4e74a611
add_recdef: actual simpset;
add_recdef_x: named simpset;

diff -r e36581d04eee -r 48f90bc10cf5 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Thu Apr 22 12:49:34 1999 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Thu Apr 22 12:50:39 1999 +0200
@@ -11,7 +11,7 @@
   val print_recdefs: theory -> unit
   val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
   val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
-    -> string option -> (xstring * Args.src list) list
+    -> simpset option -> (xstring * Args.src list) list
     -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
   val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
     -> simpset option -> (thm * theory attribute list) list
@@ -77,6 +77,7 @@
     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
     val bname = Sign.base_name name;
 
+    val _ = Theory.requires thy "Recdef" "recursive function definitions";
     val _ = message ("Defining recursive function " ^ quote name ^ " ...");
 
     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
@@ -94,9 +95,9 @@
       |> Theory.parent_path;
   in (thy3, result) end;
 
-val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute
+val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems;
+val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute
   (Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems;
-
 val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
 
 
@@ -113,9 +114,9 @@
 
 val recdef_decl =
   name -- term -- Scan.repeat1 (opt_thm_name ":" -- term) --
-  Scan.optional ($$$ "congs" |-- !!! xthms1) [] --
-  Scan.option ($$$ "simpset" |-- !!! name)
-  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef f R (map triple_swap eqs) ss congs);
+  Scan.optional ($$$ "(" |-- $$$ "congs" |-- !!! (xthms1 --| $$$ ")")) [] --
+  Scan.option ($$$ "(" |-- $$$ "simpset" |-- !!! (name --| $$$ ")"))
+  >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map triple_swap eqs) ss congs);
 
 val recdefP =
   OuterSyntax.command "recdef" "define general recursive functions (TFL)"