# 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 =