# HG changeset patch # User wenzelm # Date 1166021254 -3600 # Node ID 153fad1e7318bbea07f8138639511f37c8721c0e # Parent 7d4debbb1abf619a112bffa3803e35a6b0cd9f2a target_abbrev: internal mode for abbrevs; tuned; diff -r 7d4debbb1abf -r 153fad1e7318 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Dec 13 15:47:33 2006 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Dec 13 15:47:34 2006 +0100 @@ -290,7 +290,7 @@ val do_abbrevs = abbrevs andalso not (Output.has_mode "no_abbrevs"); val t' = t |> do_abbrevs ? rewrite_term true thy (Consts.abbrevs_of consts (! print_mode @ [""])) - |> do_abbrevs ? rewrite_term false thy (Consts.abbrevs_of consts [#1 Syntax.internal_mode]) + |> do_abbrevs ? rewrite_term false thy (Consts.abbrevs_of consts [Syntax.internalM]) |> Sign.extern_term (Consts.extern_early consts) thy |> LocalSyntax.extern_term syntax; in Sign.pretty_term' ctxt (LocalSyntax.syn_of syntax) (Consts.extern consts) t' end; @@ -910,12 +910,12 @@ fun target_abbrev prmode ((c, mx), rhs) phi = let - val mode = #1 prmode; val c' = Morphism.name phi c; val rhs' = Morphism.term phi rhs; val arg' = (c', rhs'); in - Context.mapping_result (Sign.add_abbrev mode arg') (add_abbrev mode arg') + Context.mapping_result + (Sign.add_abbrev Syntax.internalM arg') (add_abbrev Syntax.internalM arg') #-> (fn (lhs, _) => Term.equiv_types (rhs, rhs') ? target_notation prmode [(lhs, mx)] Morphism.identity) end;