Simplified primrec - definitions.

--- a/src/HOL/ex/BT.thy	Tue Jul 30 18:03:11 1996 +0200
+++ b/src/HOL/ex/BT.thy	Tue Jul 30 18:05:22 1996 +0200
@@ -20,31 +20,32 @@
     postorder   :: 'a bt => 'a list
 
 primrec n_nodes bt
-  n_nodes_Lf "n_nodes (Lf) = 0"
-  n_nodes_Br "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
+  "n_nodes (Lf) = 0"
+  "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
 
 primrec n_leaves bt
-  n_leaves_Lf "n_leaves (Lf) = Suc 0"
-  n_leaves_Br "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
+  "n_leaves (Lf) = Suc 0"
+  "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
 
 primrec reflect bt
-  reflect_Lf "reflect (Lf) = Lf"
-  reflect_Br "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
+  "reflect (Lf) = Lf"
+  "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
 
 primrec bt_map bt
-  bt_map_Lf  "bt_map f Lf = Lf"
-  bt_map_Br  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
+  "bt_map f Lf = Lf"
+  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
 
 primrec preorder bt
-  preorder_Lf "preorder (Lf) = []"
-  preorder_Br "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
+  "preorder (Lf) = []"
+  "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
 
 primrec inorder bt
-  inorder_Lf "inorder (Lf) = []"
-  inorder_Br "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
+  "inorder (Lf) = []"
+  "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
 
 primrec postorder bt
-  postorder_Lf "postorder (Lf) = []"
-  postorder_Br "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
+  "postorder (Lf) = []"
+  "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
 
 end
+

--- a/src/HOL/ex/InSort.thy	Tue Jul 30 18:03:11 1996 +0200
+++ b/src/HOL/ex/InSort.thy	Tue Jul 30 18:05:22 1996 +0200
@@ -13,9 +13,10 @@
   insort :: [['a,'a]=>bool, 'a list] => 'a list
 
 primrec ins List.list
-  ins_Nil  "ins f x [] = [x]"
-  ins_Cons "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))"
+  "ins f x [] = [x]"
+  "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))"
 primrec insort List.list
-  insort_Nil  "insort f [] = []"
-  insort_Cons "insort f (x#xs) = ins f x (insort f xs)"
+  "insort f [] = []"
+  "insort f (x#xs) = ins f x (insort f xs)"
 end
+