# HG changeset patch
# User krauss
# Date 1174578817 -3600
# Node ID baee64dbe8ea5d4a532981175decf79f8d6951aa
# Parent  cb41c397a699d37d0ec36cdec77073842ef42724
fixed function syntax

diff -r cb41c397a699 -r baee64dbe8ea src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Thu Mar 22 16:34:03 2007 +0100
+++ b/src/HOL/Nominal/Examples/SOS.thy	Thu Mar 22 16:53:37 2007 +0100
@@ -66,7 +66,7 @@
   lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm"   
 where
   "lookup [] x        = Var x"
-  "lookup ((y,e)#\<theta>) x = (if x=y then e else lookup \<theta> x)"
+| "lookup ((y,e)#\<theta>) x = (if x=y then e else lookup \<theta> x)"
 
 lemma lookup_eqvt:
   fixes pi::"name prm"