--- a/src/HOL/Nominal/Examples/LocalWeakening.thy Fri Dec 12 12:14:02 2008 +0100
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy Sat Dec 13 13:24:45 2008 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
(* Formalisation of weakening using locally nameless *)
(* terms; the nominal infrastructure can also derive *)
(* strong induction principles for such representations *)
@@ -29,13 +27,13 @@
by (induct t rule: llam.induct)
(auto simp add: llam.inject)
-consts llam_size :: "llam \<Rightarrow> nat"
-
nominal_primrec
- "llam_size (lPar a) = 1"
- "llam_size (lVar n) = 1"
- "llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)"
- "llam_size (lLam t) = 1 + (llam_size t)"
+ llam_size :: "llam \<Rightarrow> nat"
+where
+ "llam_size (lPar a) = 1"
+| "llam_size (lVar n) = 1"
+| "llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)"
+| "llam_size (lLam t) = 1 + (llam_size t)"
by (rule TrueI)+
function