# HG changeset patch
# User wenzelm
# Date 1192899273 -7200
# Node ID 23fbc38f643282ed3311fa0f00f25258d89978f6
# Parent  192105867f2540255d4c73bf36d1c36bda212556
tuned abbrev interface;

diff -r 192105867f25 -r 23fbc38f6432 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Oct 20 18:54:33 2007 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Oct 20 18:54:33 2007 +0200
@@ -25,7 +25,7 @@
     ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
     -> (term list * (bstring * thm list) list) * local_theory
   val abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory ->
-    (term * thm) * local_theory
+    (term * term) * local_theory
   val define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
     (term * (bstring * thm)) * local_theory
   val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
@@ -57,7 +57,7 @@
   axioms: string ->
     ((bstring * typ) * mixfix) list * ((bstring * Attrib.src list) * term list) list -> local_theory
     -> (term list * (bstring * thm list) list) * local_theory,
-  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * thm) * local_theory,
+  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * term) * local_theory,
   define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
     (term * (bstring * thm)) * local_theory,
   notes: string ->