# HG changeset patch
# User berghofe
# Date 836569379 -7200
# Node ID afa622bc829d1fc9fd24dc34a8f683ee4097988e
# Parent  791e794739668596a0a683decffe22a58c84bb83
Simplified syntax of primrec definitions.

diff -r 791e79473966 -r afa622bc829d src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Fri Jun 28 15:30:55 1996 +0200
+++ b/src/HOL/thy_syntax.ML	Fri Jul 05 14:22:59 1996 +0200
@@ -172,7 +172,7 @@
 
 (** primrec **)
 
-fun mk_primrec_decl ((fname, tname), axms) =
+fun mk_primrec_decl_1 ((fname, tname), axms) =
   let
     (*Isolate type name from the structure's identifier it may be stored in*)
     val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
@@ -188,8 +188,25 @@
       ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
   end;
 
+fun mk_primrec_decl_2 ((fname, tname), axms) =
+  let
+    (*Isolate type name from the structure's identifier it may be stored in*)
+    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
+
+    fun mk_prove eqn =
+      "prove_goalw thy [get_def thy "
+      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
+      \(fn _ => [Simp_tac 1])";
+
+    val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
+  in ("|> " ^ tname ^ "_add_primrec " ^ axs,
+      "val dummy = Addsimps " ^
+      brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
+  end;
+
 val primrec_decl =
-  name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl;
+  (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
+  (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;