less aggressive Assumption.export_term (similar to Generic_Target.abbrev): merely expand local defs and thus allow notation for local fixes;

--- 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;