# HG changeset patch
# User wenzelm
# Date 1192313886 -7200
# Node ID 17c845095a4710cac4fce831c5a9e6b0af950efb
# Parent  0615bb9955dddcebf4ad4eba1b276cfb58e7b957
added add_def;

diff -r 0615bb9955dd -r 17c845095a47 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sun Oct 14 00:18:05 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sun Oct 14 00:18:06 2007 +0200
@@ -14,6 +14,7 @@
   val def_export: Assumption.export
   val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     (term * (bstring * thm)) list * Proof.context
+  val add_def: (string * mixfix) * term -> Proof.context -> (term * (bstring * thm)) * Proof.context
   val export: Proof.context -> Proof.context -> thm -> thm list * thm
   val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
   val trans_terms: Proof.context -> thm list -> thm
@@ -41,8 +42,8 @@
 
 fun cert_def ctxt eq =
   let
-    val display_term = quote o Syntax.string_of_term ctxt;
-    fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
+    fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^
+      quote (Syntax.string_of_term ctxt eq));
     val ((lhs, _), eq') = eq
       |> Sign.no_vars (Syntax.pp ctxt)
       |> PrimitiveDefs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
@@ -100,6 +101,8 @@
     |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
   end;
 
+fun add_def (var, rhs) = add_defs [(var, (("", []), rhs))] #>> the_single;
+
 
 (* specific export -- result based on educated guessing *)