# HG changeset patch
# User wenzelm
# Date 1357407749 -3600
# Node ID 20e6e1a92e54bf6863945fae4f28b1a95f65acaa
# Parent  21098a5772942a5fa6373cf77ba1cd7fd9b9504b
less aggressive Assumption.export_term (similar to Generic_Target.abbrev): merely expand local defs and thus allow notation for local fixes;

diff -r 21098a577294 -r 20e6e1a92e54 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Jan 05 18:36:02 2013 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sat Jan 05 18:42:29 2013 +0100
@@ -256,13 +256,17 @@
 (* notation *)
 
 fun type_notation add mode raw_args lthy =
-  let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args in
+  let
+    val args = map (apfst (Logic.type_map (Assumption.export_term lthy (target_of lthy)))) raw_args;
+  in
     declaration {syntax = true, pervasive = false}
       (Proof_Context.generic_type_notation add mode args) lthy
   end;
 
 fun notation add mode raw_args lthy =
-  let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args in
+  let
+    val args = map (apfst (Assumption.export_term lthy (target_of lthy))) raw_args
+  in
     declaration {syntax = true, pervasive = false}
       (Proof_Context.generic_notation add mode args) lthy
   end;