# HG changeset patch
# User haftmann
# Date 1188207256 -7200
# Node ID c588ec4cf1947307c1ac75e988dfd1052be1b993
# Parent  4a405457e9d60f98b5603da14052adb65872979d
added simple definition scheme

diff -r 4a405457e9d6 -r c588ec4cf194 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Aug 27 11:34:14 2007 +0200
+++ b/src/Pure/pure_thy.ML	Mon Aug 27 11:34:16 2007 +0200
@@ -84,6 +84,8 @@
     theory -> thm list list * theory
   val add_axiomss_i: ((bstring * term list) * attribute list) list ->
     theory -> thm list list * theory
+  val simple_def: bstring * attribute list ->
+    ((bstring * typ * mixfix) * term list) * term -> theory -> (string * thm) * theory
   val add_defs: bool -> ((bstring * string) * attribute list) list ->
     theory -> thm list * theory
   val add_defs_i: bool -> ((bstring * term) * attribute list) list ->
@@ -488,6 +490,21 @@
 end;
 
 
+(* simple interface for simple definitions *)
+
+fun simple_def (raw_name, atts) (((raw_c, ty, syn), ts), t) thy =
+  let
+    val c = Sign.full_name thy raw_c;
+    val name = if raw_name = "" then Thm.def_name raw_c else raw_name;
+    val def = Logic.mk_equals (list_comb (Const (c, ty), ts), t);
+  in
+    thy
+    |> Sign.add_consts_authentic [(raw_c, ty, syn)]
+    |> add_defs_i false [((name, def), atts)]
+    |-> (fn [thm] => pair (c, thm))
+  end;
+
+
 
 (*** the ProtoPure theory ***)