src/HOL/Nominal/Examples/W.thy

--- a/src/HOL/Nominal/Examples/W.thy	Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/Nominal/Examples/W.thy	Wed Sep 08 19:21:46 2010 +0200
@@ -150,12 +150,9 @@
 equivariance valid
 
 text {* General *}
-consts
-  gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS"
-
-primrec 
+primrec gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS" where
   "gen T [] = Ty T"
-  "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
+| "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
 
 lemma gen_eqvt[eqvt]:
   fixes pi::"tvar prm"