# HG changeset patch
# User wenzelm
# Date 1459774410 -7200
# Node ID eeea384cafc847eafb53ba736295c7f802c609e2
# Parent  db9f95ca2a8fc17c78a1e0c6c49634761bc1939b
avoid duplicate reports;

diff -r db9f95ca2a8f -r eeea384cafc8 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Apr 04 14:53:30 2016 +0200
@@ -309,17 +309,21 @@
 fun type_notation add mode raw_args lthy =
   let
     val args = map (apfst (Logic.type_map (Assumption.export_term lthy (target_of lthy)))) raw_args;
+    val args' = map (apsnd Mixfix.reset_pos) args;
+    val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args;
   in
     declaration {syntax = true, pervasive = false}
-      (Proof_Context.generic_type_notation add mode args) lthy
+      (Proof_Context.generic_type_notation add mode args') lthy
   end;
 
 fun notation add mode raw_args lthy =
   let
     val args = map (apfst (Assumption.export_term lthy (target_of lthy))) raw_args
+    val args' = map (apsnd Mixfix.reset_pos) args;
+    val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args;
   in
     declaration {syntax = true, pervasive = false}
-      (Proof_Context.generic_notation add mode args) lthy
+      (Proof_Context.generic_notation add mode args') lthy
   end;