# HG changeset patch
# User wenzelm
# Date 1192820234 -7200
# Node ID 26b9a7db338679ea8c089eae3cb530f9bb7fca5d
# Parent  1ee419a5a30f27fd1a814bc2318cfecd5d3f732a
tuned interfaces;

diff -r 1ee419a5a30f -r 26b9a7db3386 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Oct 19 19:45:31 2007 +0200
+++ b/src/Pure/Isar/class.ML	Fri Oct 19 20:57:14 2007 +0200
@@ -20,9 +20,9 @@
   val these_params: theory -> sort -> (string * (string * typ)) list
   val init: class -> Proof.context -> Proof.context
   val add_logical_const: string -> Markup.property list
-    -> (string * mixfix) * term -> theory -> string * theory
+    -> (string * mixfix) * term -> theory -> theory
   val add_syntactic_const: string -> Syntax.mode -> Markup.property list
-    -> (string * mixfix) * term -> theory -> string * theory
+    -> (string * mixfix) * term -> theory -> theory
   val refresh_syntax: class -> Proof.context -> Proof.context
   val intro_classes_tac: thm list -> tactic
   val default_intro_classes_tac: thm list -> tactic
@@ -827,7 +827,6 @@
           #> register_operation class ((c', (dict, dict')), SOME (Thm.varifyT def)))
     |> Sign.restore_naming thy
     |> Sign.add_const_constraint (c', SOME ty')
-    |> pair c'
   end;
 
 
@@ -872,7 +871,6 @@
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
     |> register_operation class ((c', (dict', dict'')), NONE)
     |> Sign.restore_naming thy
-    |> pair c'
   end;
 
 end;
diff -r 1ee419a5a30f -r 26b9a7db3386 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Fri Oct 19 19:45:31 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Fri Oct 19 20:57:14 2007 +0200
@@ -14,7 +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 add_def: (string * mixfix) * term -> Proof.context -> (term * 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
@@ -101,7 +101,9 @@
     |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
   end;
 
-fun add_def (var, rhs) = add_defs [(var, (("", []), rhs))] #>> the_single;
+fun add_def (var, rhs) ctxt =
+  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (("", []), rhs))] ctxt
+  in ((lhs, th), ctxt') end;
 
 
 (* specific export -- result based on educated guessing *)
diff -r 1ee419a5a30f -r 26b9a7db3386 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Oct 19 19:45:31 2007 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Oct 19 20:57:14 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 * (bstring * thm)) * local_theory
+    (term * thm) * 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,8 +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 * (bstring * thm)) * local_theory,
+  abbrev: Syntax.mode -> (bstring * mixfix) * term -> local_theory -> (term * thm) * local_theory,
   define: string -> (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory ->
     (term * (bstring * thm)) * local_theory,
   notes: string ->