# HG changeset patch
# User wenzelm
# Date 1333388841 -7200
# Node ID fc95b8b6c260e62cda61143979a781c41cc1a0ed
# Parent  feef9b0b6031847cb1ff7d26a19bedea166e0833
tuned signature;

diff -r feef9b0b6031 -r fc95b8b6c260 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Mon Apr 02 19:10:52 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Apr 02 19:47:21 2012 +0200
@@ -51,7 +51,7 @@
     let
       val b' = Morphism.binding phi b;
       val rhs' = Morphism.term phi rhs;
-      val arg = (b', Term.close_schematic_term rhs');
+      val rhs'' = Term.close_schematic_term rhs';
       val same_shape = Term.aconv_untyped (rhs, rhs');
 
       (* FIXME workaround based on educated guess *)
@@ -63,13 +63,10 @@
         orelse same_shape);
     in
       not is_canonical_class ?
-        (Context.mapping_result
-          (Sign.add_abbrev Print_Mode.internal arg)
-          (Proof_Context.add_abbrev Print_Mode.internal arg)
+        (Proof_Context.generic_add_abbrev Print_Mode.internal (b', rhs'')
         #-> (fn (lhs' as Const (d, _), _) =>
             same_shape ?
-              (Context.mapping
-                (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
+              (Proof_Context.generic_revert_abbrev mode d #>
                Morphism.form (Proof_Context.generic_notation true prmode [(lhs', mx)]))))
     end);
 
diff -r feef9b0b6031 -r fc95b8b6c260 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Apr 02 19:10:52 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Apr 02 19:47:21 2012 +0200
@@ -146,6 +146,9 @@
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
+  val generic_add_abbrev: string -> binding * term -> Context.generic ->
+    (term * term) * Context.generic
+  val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
   val print_binds: Proof.context -> unit
@@ -1021,6 +1024,12 @@
 
 fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c);
 
+fun generic_add_abbrev mode arg =
+  Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg);
+
+fun generic_revert_abbrev mode arg =
+  Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg);
+
 
 (* fixes *)