# HG changeset patch
# User wenzelm
# Date 1165952969 -3600
# Node ID e024aa65f4cefb397f9708822fc6ff64eead8cb9
# Parent  c77bc21b3eef776f3aef9fa91cd99f5bc65054ea
abbrev: tuned signature;

diff -r c77bc21b3eef -r e024aa65f4ce src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Dec 12 20:49:28 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Tue Dec 12 20:49:29 2006 +0100
@@ -24,7 +24,8 @@
     ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory
   val axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
     (bstring * thm list) list * local_theory
-  val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> local_theory
+  val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
+    (term * term) * local_theory
   val defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list ->
     local_theory -> (term * (bstring * thm)) list * local_theory
   val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
@@ -58,7 +59,7 @@
     (term * thm) list * local_theory,
   axioms: string -> ((bstring * Attrib.src list) * term list) list -> local_theory ->
     (bstring * thm list) list * local_theory,
-  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> local_theory,
+  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
   defs: string -> ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list ->
     local_theory -> (term * (bstring * thm)) list * local_theory,
   notes: string ->