src/HOL/BNF/Examples/Misc_Primrec.thy
changeset 54193 bc07627c5dcd
parent 54019 1878bab3e1c9
--- a/src/HOL/BNF/Examples/Misc_Primrec.thy	Wed Oct 23 09:58:30 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Primrec.thy	Wed Oct 23 14:53:36 2013 +0200
@@ -14,7 +14,7 @@
 primrec_new nat_of_simple :: "simple \<Rightarrow> nat" where
   "nat_of_simple X1 = 1" |
   "nat_of_simple X2 = 2" |
-  "nat_of_simple X3 = 2" |
+  "nat_of_simple X3 = 3" |
   "nat_of_simple X4 = 4"
 
 primrec_new simple_of_simple' :: "simple' \<Rightarrow> simple" where