# HG changeset patch
# User berghofe
# Date 901832285 -7200
# Node ID 7e9f9ab61798f9a7c4b8b76f6101a1ffa47e4d02
# Parent  07f80f447b27c7e38473f887301dddf175d46008
Fixed primrec.

diff -r 07f80f447b27 -r 7e9f9ab61798 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Thu Jul 30 19:18:50 1998 +0200
+++ b/src/HOL/thy_syntax.ML	Thu Jul 30 22:58:05 1998 +0200
@@ -186,16 +186,16 @@
 
 (** primrec **)
 
-fun mk_primrec_decl (names, eqns) =
+fun mk_primrec_decl (alt_name, (names, eqns)) =
   ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^
-  ") = PrimrecPackage.add_primrec None " ^ brackets (commas_quote names) ^ " " ^
-    brackets (commas eqns) ^ " thy;\n\
+  ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
+    brackets (commas_quote names) ^ " " ^ brackets (commas eqns) ^ " thy;\n\
   \val thy = thy\n";
 
 (* either names and axioms or just axioms *)
-val primrec_decl =
-  (repeat1 (ident -- string) >> (mk_primrec_decl o ListPair.unzip)) ||
-  (repeat1 string >> (mk_primrec_decl o (pair [])));
+val primrec_decl = (optional ("(" $$-- name --$$ ")" >> (cat "Some")) "None" --
+  ((repeat1 (ident -- string) >> ListPair.unzip) ||
+   (repeat1 string >> (pair [])))) >> mk_primrec_decl;
 
 
 (** rec: interface to Slind's TFL **)