--- 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);
--- 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 *)