# HG changeset patch
# User wenzelm
# Date 1335210823 -7200
# Node ID 5f9ce06f281e1496730c795eca7ef050787c4be2
# Parent  157e6108a342a6234997a30b6f02140fe4dbaa13
typedef with implicit set definition is considered legacy;

diff -r 157e6108a342 -r 5f9ce06f281e NEWS
--- a/NEWS	Mon Apr 23 21:44:36 2012 +0200
+++ b/NEWS	Mon Apr 23 21:53:43 2012 +0200
@@ -187,6 +187,10 @@
 
 * New type synonym 'a rel = ('a * 'a) set
 
+* Typedef with implicit set definition is considered legacy.  Use
+"typedef (open)" form instead, which will eventually become the
+default.
+
 * More default pred/set conversions on a couple of relation operations
 and predicates.  Added powers of predicate relations.  Consolidation
 of some relation theorems:
diff -r 157e6108a342 -r 5f9ce06f281e src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Apr 23 21:44:36 2012 +0200
+++ b/src/HOL/Tools/typedef.ML	Mon Apr 23 21:53:43 2012 +0200
@@ -308,8 +308,11 @@
       (Parse.type_args_constrained -- Parse.binding) --
         Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
         Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
-    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
-        typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
+    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy =>
+          (if def then
+            legacy_feature "typedef with implicit set definition -- use \"typedef (open)\" instead"
+           else ();
+           typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) lthy)));
 
 end;