1.1 --- a/src/HOL/HOL.thy	Fri Oct 24 17:48:33 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Oct 24 17:48:34 2008 +0200
     1.3 @@ -202,11 +202,8 @@
     1.4  axiomatization
     1.5    undefined :: 'a
     1.6  
     1.7 -consts
     1.8 -  arbitrary :: 'a
     1.9 -
    1.10 -finalconsts
    1.11 -  arbitrary
    1.12 +abbreviation (input)
    1.13 +  "arbitrary \<equiv> undefined"
    1.14  
    1.15  
    1.16  subsubsection {* Generic classes and algebraic operations *}