diff -r 7b2631c91a95 -r 9e58f0499f57 src/HOL/ex/Chinese.thy
--- a/src/HOL/ex/Chinese.thy	Wed Sep 08 13:25:22 2010 +0200
+++ b/src/HOL/ex/Chinese.thy	Wed Sep 08 19:21:46 2010 +0200
@@ -1,5 +1,4 @@
 (* -*- coding: utf-8 -*- :encoding=utf-8:
-    ID:         $Id$
     Author:     Ning Zhang and Christian Urban
 
 Example theory involving Unicode characters (UTF-8 encoding) -- both
@@ -30,20 +29,17 @@
   | Nine  ("九")
   | Ten   ("十")
 
-consts
-  translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100)
-
-primrec
+primrec translate :: "shuzi \<Rightarrow> nat" ("|_|" [100] 100) where
  "|一| = 1"
- "|二| = 2"
- "|三| = 3"
- "|四| = 4"
- "|五| = 5"
- "|六| = 6"
- "|七| = 7"
- "|八| = 8"
- "|九| = 9"
- "|十| = 10"
+|"|二| = 2"
+|"|三| = 3"
+|"|四| = 4"
+|"|五| = 5"
+|"|六| = 6"
+|"|七| = 7"
+|"|八| = 8"
+|"|九| = 9"
+|"|十| = 10"
 
 thm translate.simps