1.1 --- a/NEWS	Sat Mar 17 00:17:30 2012 +0100
     1.2 +++ b/NEWS	Sat Mar 17 09:51:18 2012 +0100
     1.3 @@ -48,6 +48,10 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Command 'definition' no longer exports the foundational "raw_def"
     1.8 +into the user context.  Minor INCOMPATIBILITY, may use the regular
     1.9 +"def" result with attribute "abs_def" to imitate the old version.
    1.10 +
    1.11  * Attribute "abs_def" turns an equation of the form "f x y == t" into
    1.12  "f == %x y. t", which ensures that "simp" or "unfold" steps always
    1.13  expand it.  This also works for object-logic equality.  (Formerly

     2.1 --- a/src/HOL/Orderings.thy	Sat Mar 17 00:17:30 2012 +0100
     2.2 +++ b/src/HOL/Orderings.thy	Sat Mar 17 09:51:18 2012 +0100
     2.3 @@ -1314,7 +1314,6 @@
     2.4  
     2.5  definition
     2.6    [no_atp]: "\<top> = (\<lambda>x. \<top>)"
     2.7 -declare top_fun_def_raw [no_atp]
     2.8  
     2.9  lemma top_apply [simp] (* CANDIDATE [code] *):
    2.10    "\<top> x = \<top>"

     3.1 --- a/src/HOL/Quickcheck.thy	Sat Mar 17 00:17:30 2012 +0100
     3.2 +++ b/src/HOL/Quickcheck.thy	Sat Mar 17 09:51:18 2012 +0100
     3.3 @@ -262,16 +262,17 @@
     3.4    where "map f P = bind P (single o f)"
     3.5  
     3.6  hide_fact
     3.7 -  random_bool_def random_bool_def_raw
     3.8 -  random_itself_def random_itself_def_raw
     3.9 -  random_char_def random_char_def_raw
    3.10 -  random_literal_def random_literal_def_raw
    3.11 -  random_nat_def random_nat_def_raw
    3.12 -  random_int_def random_int_def_raw
    3.13 -  random_fun_lift_def random_fun_lift_def_raw
    3.14 -  random_fun_def random_fun_def_raw
    3.15 -  collapse_def collapse_def_raw
    3.16 -  beyond_def beyond_def_raw beyond_zero
    3.17 +  random_bool_def
    3.18 +  random_itself_def
    3.19 +  random_char_def
    3.20 +  random_literal_def
    3.21 +  random_nat_def
    3.22 +  random_int_def
    3.23 +  random_fun_lift_def
    3.24 +  random_fun_def
    3.25 +  collapse_def
    3.26 +  beyond_def
    3.27 +  beyond_zero
    3.28    random_aux_rec
    3.29  
    3.30  hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Mar 17 00:17:30 2012 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Mar 17 09:51:18 2012 +0100
     4.3 @@ -867,8 +867,7 @@
     4.4              (not (Config.get ctxt ignore_no_atp) andalso
     4.5               is_package_def name0) orelse
     4.6              exists (fn s => String.isSuffix s name0)
     4.7 -                   (multi_base_blacklist ctxt ho_atp) orelse
     4.8 -            String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
     4.9 +                   (multi_base_blacklist ctxt ho_atp)) then
    4.10            I
    4.11          else
    4.12            let