# HG changeset patch
# User wenzelm
# Date 1331974278 -3600
# Node ID 80123a2202194dc7d260131cd765f04e35fe679d
# Parent  c54ca5717f73c43c0dc655ddc3e8fc9caa3de56a
'definition' no longer exports the foundational "raw_def";

diff -r c54ca5717f73 -r 80123a220219 NEWS
--- a/NEWS	Sat Mar 17 00:17:30 2012 +0100
+++ b/NEWS	Sat Mar 17 09:51:18 2012 +0100
@@ -48,6 +48,10 @@
 
 *** Pure ***
 
+* Command 'definition' no longer exports the foundational "raw_def"
+into the user context.  Minor INCOMPATIBILITY, may use the regular
+"def" result with attribute "abs_def" to imitate the old version.
+
 * Attribute "abs_def" turns an equation of the form "f x y == t" into
 "f == %x y. t", which ensures that "simp" or "unfold" steps always
 expand it.  This also works for object-logic equality.  (Formerly
diff -r c54ca5717f73 -r 80123a220219 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Mar 17 00:17:30 2012 +0100
+++ b/src/HOL/Orderings.thy	Sat Mar 17 09:51:18 2012 +0100
@@ -1314,7 +1314,6 @@
 
 definition
   [no_atp]: "\<top> = (\<lambda>x. \<top>)"
-declare top_fun_def_raw [no_atp]
 
 lemma top_apply [simp] (* CANDIDATE [code] *):
   "\<top> x = \<top>"
diff -r c54ca5717f73 -r 80123a220219 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Sat Mar 17 00:17:30 2012 +0100
+++ b/src/HOL/Quickcheck.thy	Sat Mar 17 09:51:18 2012 +0100
@@ -262,16 +262,17 @@
   where "map f P = bind P (single o f)"
 
 hide_fact
-  random_bool_def random_bool_def_raw
-  random_itself_def random_itself_def_raw
-  random_char_def random_char_def_raw
-  random_literal_def random_literal_def_raw
-  random_nat_def random_nat_def_raw
-  random_int_def random_int_def_raw
-  random_fun_lift_def random_fun_lift_def_raw
-  random_fun_def random_fun_def_raw
-  collapse_def collapse_def_raw
-  beyond_def beyond_def_raw beyond_zero
+  random_bool_def
+  random_itself_def
+  random_char_def
+  random_literal_def
+  random_nat_def
+  random_int_def
+  random_fun_lift_def
+  random_fun_def
+  collapse_def
+  beyond_def
+  beyond_zero
   random_aux_rec
 
 hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
diff -r c54ca5717f73 -r 80123a220219 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Mar 17 00:17:30 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Mar 17 09:51:18 2012 +0100
@@ -867,8 +867,7 @@
             (not (Config.get ctxt ignore_no_atp) andalso
              is_package_def name0) orelse
             exists (fn s => String.isSuffix s name0)
-                   (multi_base_blacklist ctxt ho_atp) orelse
-            String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
+                   (multi_base_blacklist ctxt ho_atp)) then
           I
         else
           let