# HG changeset patch
# User urbanc
# Date 1129563634 -7200
# Node ID 67ffbfcd6fefb312fd3084f53c0ccee98ceaee13
# Parent  c35381811d5c45ec8ed4adbfc3ca86a42f58bc9f
deleted leading space in the definition of fresh

diff -r c35381811d5c -r 67ffbfcd6fef src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Oct 17 12:30:57 2005 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Oct 17 17:40:34 2005 +0200
@@ -101,7 +101,7 @@
    supp :: "'a \<Rightarrow> ('x set)"  
    "supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
 
-   fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" (" _ \<sharp> _" [80,80] 80)
+   fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80)
    "a \<sharp> x \<equiv> a \<notin> supp x"
 
    supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl 80)