diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/FunDef.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -108,7 +108,7 @@
 section {* Definitions with default value *}
 
 definition
-  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
+  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
   "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
 
 lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
@@ -178,9 +178,9 @@
 inductive rpg
 intros
   "(Inr y, y) : rpg"
-definition
-  "lproj x = (THE y. (x,y) : lpg)"
-  "rproj x = (THE y. (x,y) : rpg)"
+
+definition "lproj x = (THE y. (x,y) : lpg)"
+definition "rproj x = (THE y. (x,y) : rpg)"
 
 lemma lproj_inl:
   "lproj (Inl x) = x"