# HG changeset patch
# User haftmann
# Date 1197036487 -3600
# Node ID 0c9052719f20c8b25ebbaf09abf3eb9ca3b6efad
# Parent  c9e39eafc7a0318bb6b2f031d71d6c892c1afe34
new primrec

diff -r c9e39eafc7a0 -r 0c9052719f20 src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Fri Dec 07 15:07:59 2007 +0100
+++ b/src/HOL/ex/ExecutableContent.thy	Fri Dec 07 15:08:07 2007 +0100
@@ -39,15 +39,14 @@
 datatype mut1 = Tip | Top mut2
   and mut2 = Tip | Top mut1
 
-consts
+primrec
   mut1 :: "mut1 \<Rightarrow> mut1"
-  mut2 :: "mut2 \<Rightarrow> mut2"
-
-primrec
+  and mut2 :: "mut2 \<Rightarrow> mut2"
+where
   "mut1 mut1.Tip = mut1.Tip"
-  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
-  "mut2 mut2.Tip = mut2.Tip"
-  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
+  | "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
+  | "mut2 mut2.Tip = mut2.Tip"
+  | "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
 
 definition
   "mystring = ''my home is my castle''"