# HG changeset patch
# User wenzelm
# Date 1148161017 -7200
# Node ID 877b763ded7eff989d886d68b556dc118f2e5f46
# Parent  0a7c6d78ad6b6fc6565b888dd855c3d6b973cedd
added syntax for 'unchecked';

diff -r 0a7c6d78ad6b -r 877b763ded7e src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Sat May 20 23:36:56 2006 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Sat May 20 23:36:57 2006 +0200
@@ -10,6 +10,8 @@
   val quiet_mode: bool ref
   val add_primrec: string -> ((bstring * string) * Attrib.src list) list
     -> theory -> theory * thm list
+  val add_primrec_unchecked: string -> ((bstring * string) * Attrib.src list) list
+    -> theory -> theory * thm list
   val add_primrec_i: string -> ((bstring * term) * attribute list) list
     -> theory -> theory * thm list
   val add_primrec_unchecked_i: string -> ((bstring * term) * attribute list) list
@@ -223,7 +225,7 @@
     |> RuleCases.save induction
   end;
 
-fun gen_primrec unchecked alt_name eqns_atts thy =
+fun gen_primrec_i unchecked alt_name eqns_atts thy =
   let
     val (eqns, atts) = split_list eqns_atts;
     val sg = Theory.sign_of thy;
@@ -269,10 +271,7 @@
     (thy''', simps')
   end;
 
-val add_primrec_i = gen_primrec false;
-val add_primrec_unchecked_i = gen_primrec true;
-
-fun add_primrec alt_name eqns thy =
+fun gen_primrec unchecked alt_name eqns thy =
   let
     val sign = Theory.sign_of thy;
     val ((names, strings), srcss) = apfst split_list (split_list eqns);
@@ -283,22 +282,33 @@
       handle TERM _ => primrec_eq_err sign "not a proper equation" eq) eqn_ts;
     val (_, eqn_ts') = InductivePackage.unify_consts (sign_of thy) rec_ts eqn_ts
   in
-    add_primrec_i alt_name (names ~~ eqn_ts' ~~ atts) thy
+    gen_primrec_i unchecked alt_name (names ~~ eqn_ts' ~~ atts) thy
   end;
 
+val add_primrec = gen_primrec false;
+val add_primrec_unchecked = gen_primrec true;
+val add_primrec_i = gen_primrec_i false;
+val add_primrec_unchecked_i = gen_primrec_i true;
+
 
 (* outer syntax *)
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val opt_unchecked_name =
+  Scan.optional (P.$$$ "(" |-- P.!!!
+    (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
+      P.name >> pair false) --| P.$$$ ")")) (false, "");
+
 val primrec_decl =
-  Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
-    Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
+  opt_unchecked_name -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop);
 
 val primrecP =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
-    (primrec_decl >> (fn (alt_name, eqns) =>
-      Toplevel.theory (#1 o add_primrec alt_name (map P.triple_swap eqns))));
+    (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
+      Toplevel.theory (#1 o
+        (if unchecked then add_primrec_unchecked else add_primrec) alt_name
+          (map P.triple_swap eqns))));
 
 val _ = OuterSyntax.add_parsers [primrecP];