# HG changeset patch # User wenzelm # Date 1172696746 -3600 # Node ID 7635e59e3125fea0da8c85ee10e9e455b1dac9fb # Parent abfcb9899d41b723f6514a5e241875536e2b13ad abbrev: be permissive after transformation; diff -r abfcb9899d41 -r 7635e59e3125 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Wed Feb 28 22:05:44 2007 +0100 +++ b/src/Pure/Isar/theory_target.ML Wed Feb 28 22:05:46 2007 +0100 @@ -57,7 +57,8 @@ (* consts *) fun internal_abbrev prmode ((c, mx), t) = - LocalTheory.term_syntax (ProofContext.target_abbrev prmode ((c, mx), t)) #> + (* FIXME really permissive *) + LocalTheory.term_syntax (perhaps o try o ProofContext.target_abbrev prmode ((c, mx), t)) #> ProofContext.add_abbrev Syntax.internalM (c, t) #> snd; fun consts is_loc some_class depends decls lthy =