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