tuned recdef hints;

--- a/doc-src/IsarRef/hol.tex	Wed Sep 13 22:27:53 2000 +0200
+++ b/doc-src/IsarRef/hol.tex	Wed Sep 13 22:28:50 2000 +0200
@@ -133,6 +133,15 @@
 %  \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
+\railalias{recdefsimp}{recdef\_simp}
+\railterm{recdefsimp}
+
+\railalias{recdefcong}{recdef\_cong}
+\railterm{recdefcong}
+
+\railalias{recdefwf}{recdef\_wf}
+\railterm{recdefwf}
+
 \begin{rail}
   'primrec' parname? (equation + )
   ;
@@ -145,7 +154,7 @@
   ;
   hints: '(' 'hints' (recdefmod * ) ')'
   ;
-  recdefmod: (('simp' | 'cong' | 'wf' | 'split' | 'iff') (() | 'add' | 'del') ':' thmrefs) | clamod
+  recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   ;
 \end{rail}
 
@@ -154,10 +163,11 @@
   datatypes, see also \cite{isabelle-HOL}.
 \item [$\isarkeyword{recdef}$] defines general well-founded recursive
   functions (using the TFL package), see also \cite{isabelle-HOL}.  The
-  $simp$, $cong$, and $wf$ hints refer to auxiliary rules to be used in the
-  internal automated proof process of TFL; the other declarations refer to the
-  Simplifier and Classical reasoner (\S\ref{sec:simplifier},
-  \S\ref{sec:classical}, \S\ref{sec:clasimp}) that are used internally.
+  $recdef_simp$, $recdef_cong$, and $recdef_wf$ hints refer to auxiliary rules
+  to be used in the internal automated proof process of TFL.  Additional
+  $clasimpmod$ declarations (cf.\ \S\ref{sec:clasimp}) may be given to tune
+  the context of the Simplifier (cf.\ \S\ref{sec:simplifier}) and Classical
+  reasoner (cf.\ \S\ref{sec:classical}).
 \end{descr}
 
 Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 

--- a/src/HOL/Tools/recdef_package.ML	Wed Sep 13 22:27:53 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Wed Sep 13 22:28:50 2000 +0200
@@ -180,32 +180,27 @@
 end;
 
 
-
-(** prepare_hints(_i) **)
-
-local
+(* modifiers *)
 
-val simpN = "simp";
-val congN = "cong";
-val wfN = "wf";
-val addN = "add";
-val delN = "del";
+val recdef_simpN = "recdef_simp";
+val recdef_congN = "recdef_cong";
+val recdef_wfN = "recdef_wf";
 
 val recdef_modifiers =
- [Args.$$$ simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier),
-  Args.$$$ simpN -- Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
-  Args.$$$ congN -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ congN -- Args.$$$ addN -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ congN -- Args.$$$ delN -- Args.colon >> K (I, cong_del_local),
-  Args.$$$ wfN -- Args.colon >> K (I, wf_add_local),
-  Args.$$$ wfN -- Args.$$$ addN -- Args.colon >> K (I, wf_add_local),
-  Args.$$$ wfN -- Args.$$$ delN -- Args.colon >> K (I, wf_del_local)];
+ [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier),
+  Args.$$$ recdef_simpN -- Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
+  Args.$$$ recdef_simpN -- Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
+  Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add_local),
+  Args.$$$ recdef_congN -- Args.$$$ Args.addN -- Args.colon >> K (I, cong_add_local),
+  Args.$$$ recdef_congN -- Args.$$$ Args.delN -- Args.colon >> K (I, cong_del_local),
+  Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add_local),
+  Args.$$$ recdef_wfN -- Args.$$$ Args.addN -- Args.colon >> K (I, wf_add_local),
+  Args.$$$ recdef_wfN -- Args.$$$ Args.delN -- Args.colon >> K (I, wf_del_local)] @
+  Clasimp.clasimp_modifiers;
 
-val modifiers =  (* FIXME include 'simp cong' (!?) *)
-  recdef_modifiers @ Splitter.split_modifiers @ Classical.cla_modifiers @ Clasimp.iff_modifiers;
+
 
-in
+(** prepare_hints(_i) **)
 
 fun prepare_hints thy opt_src =
   let
@@ -213,7 +208,7 @@
     val ctxt =
       (case opt_src of
         None => ctxt0
-      | Some src => Method.only_sectioned_args modifiers I src ctxt0);
+      | Some src => Method.only_sectioned_args recdef_modifiers I src ctxt0);
     val {simps, congs, wfs} = get_local_hints ctxt;
     val cs = Classical.get_local_claset ctxt;
     val ss = Simplifier.get_local_simpset ctxt addsimps simps;
@@ -223,8 +218,6 @@
   let val {simps, congs, wfs} = get_global_hints thy
   in (Classical.claset_of thy, Simplifier.simpset_of thy addsimps simps, map #2 congs, wfs) end;
 
-end;
-
 
 
 (** add_recdef(_i) **)
@@ -305,9 +298,9 @@
 val setup =
  [GlobalRecdefData.init, LocalRecdefData.init,
   Attrib.add_attributes
-   [("recdef_simp", simp_attr, "declaration of recdef simp rule"),
-    ("recdef_cong", cong_attr, "declaration of recdef cong rule"),
-    ("recdef_wf", wf_attr, "declaration of recdef wf rule")]];
+   [(recdef_simpN, simp_attr, "declaration of recdef simp rule"),
+    (recdef_congN, cong_attr, "declaration of recdef cong rule"),
+    (recdef_wfN, wf_attr, "declaration of recdef wf rule")]];
 
 
 (* outer syntax *)
@@ -336,7 +329,6 @@
   OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
     (defer_recdef_decl >> Toplevel.theory);
 
-val _ = OuterSyntax.add_keywords ["hints"];
 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP];
 
 end;