tuned syntax, potentially more robust;

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