diff -r 95a239a5e055 -r 68245155eb58 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Fri Dec 12 12:14:02 2008 +0100
+++ b/src/HOL/Nominal/Examples/SOS.thy	Sat Dec 13 13:24:45 2008 +0100
@@ -1,4 +1,3 @@
-(* "$Id$" *)
 (*                                                        *)
 (* Formalisation of some typical SOS-proofs.              *)
 (*                                                        *) 
@@ -62,13 +61,12 @@
 
 (* parallel substitution *)
 
-consts
+nominal_primrec
   psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [95,95] 105)
- 
-nominal_primrec
+where
   "\<theta><(Var x)> = (lookup \<theta> x)"
-  "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
-  "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
+| "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
+| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)+
@@ -349,12 +347,12 @@
 using h by (induct) (auto)
 
 (* Valuation *)
-consts
-  V :: "ty \<Rightarrow> trm set" 
 
 nominal_primrec
+  V :: "ty \<Rightarrow> trm set" 
+where
   "V (TVar x) = {e. val e}"
-  "V (T\<^isub>1 \<rightarrow> T\<^isub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^isub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2}"
+| "V (T\<^isub>1 \<rightarrow> T\<^isub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^isub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2}"
   by (rule TrueI)+ 
 
 lemma V_eqvt: