# HG changeset patch
# User wenzelm
# Date 1001697686 -7200
# Node ID 481148b273b5a3e5d32e901f49606e3af5c58a3a
# Parent  e57a6e51715e4adeff3a1eaf32661163fbee2b27
permissive option;

diff -r e57a6e51715e -r 481148b273b5 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Fri Sep 28 19:19:26 2001 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Sep 28 19:21:26 2001 +0200
@@ -24,10 +24,10 @@
   val cong_del_local: Proof.context attribute
   val wf_add_local: Proof.context attribute
   val wf_del_local: Proof.context attribute
-  val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list ->
+  val add_recdef: bool -> xstring -> string -> ((bstring * string) * Args.src list) list ->
     Args.src option -> theory -> theory
       * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
-  val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list ->
+  val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list ->
     theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
   val add_recdef_old: xstring -> string -> ((bstring * string) * Args.src list) list ->
     simpset * thm list -> theory ->
@@ -228,7 +228,7 @@
 
 fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
 
-fun gen_add_recdef tfl_fn prep_att prep_hints raw_name R eq_srcs hints thy =
+fun gen_add_recdef tfl_fn prep_att prep_hints strict raw_name R eq_srcs hints thy =
   let
     val _ = requires_recdef thy;
 
@@ -240,7 +240,7 @@
     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
 
     val (cs, ss, congs, wfs) = prep_hints thy hints;
-    val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn thy cs ss congs wfs name R eqs;
+    val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn strict thy cs ss congs wfs name R eqs;
     val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
     val simp_att = if null tcs then [Simplifier.simp_add_global] else [];
 
@@ -258,7 +258,7 @@
   in (thy, result) end;
 
 val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints;
-fun add_recdef_i x y z = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z ();
+fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
 
 
 (* add_recdef_old -- legacy interface *)
@@ -267,7 +267,7 @@
   let val {simps, congs, wfs} = get_global_hints thy
   in (Classical.claset_of thy, ss addsimps simps, map #2 (add_congs thms congs), wfs) end;
 
-val add_recdef_old = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints_old;
+val add_recdef_old = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints_old false;
 
 
 
@@ -339,9 +339,10 @@
   P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
 
 val recdef_decl =
+  Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
   P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment)
     -- Scan.option hints
-  >> (fn (((f, R), eqs), src) => #1 o add_recdef f R (map P.triple_swap eqs) src);
+  >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
 
 val recdefP =
   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
@@ -369,7 +370,7 @@
     (recdef_tc_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_recdef_tc)));
 
 
-val _ = OuterSyntax.add_keywords ["congs", "hints"];
+val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];
 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP, recdef_tcP];
 
 end;