# HG changeset patch
# User wenzelm
# Date 1354113492 -3600
# Node ID 227477f17c26397c62e3fbbb7c0a57957bd2f03e
# Parent  267bd685a69f930cf0f9dd52d8c6b39d0660e906
tuned syntax, potentially more robust;

diff -r 267bd685a69f -r 227477f17c26 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Wed Nov 28 14:55:46 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Wed Nov 28 15:38:12 2012 +0100
@@ -23,7 +23,7 @@
 lemma finite_domain[simp, intro]: "finite (domain P)"
   by (cases P) (auto simp: domain_def Abs_finmap_inverse)
 
-definition proj ("_\<^isub>F" [1000] 1000) where "proj P i = snd (Rep_finmap P) i"
+definition proj ("'((_)')\<^isub>F" [0] 1000) where "proj P i = snd (Rep_finmap P) i"
 
 declare [[coercion proj]]