1.1 --- a/NEWS	Mon Apr 23 21:44:36 2012 +0200
     1.2 +++ b/NEWS	Mon Apr 23 21:53:43 2012 +0200
     1.3 @@ -187,6 +187,10 @@
     1.4  
     1.5  * New type synonym 'a rel = ('a * 'a) set
     1.6  
     1.7 +* Typedef with implicit set definition is considered legacy.  Use
     1.8 +"typedef (open)" form instead, which will eventually become the
     1.9 +default.
    1.10 +
    1.11  * More default pred/set conversions on a couple of relation operations
    1.12  and predicates.  Added powers of predicate relations.  Consolidation
    1.13  of some relation theorems:

     2.1 --- a/src/HOL/Tools/typedef.ML	Mon Apr 23 21:44:36 2012 +0200
     2.2 +++ b/src/HOL/Tools/typedef.ML	Mon Apr 23 21:53:43 2012 +0200
     2.3 @@ -308,8 +308,11 @@
     2.4        (Parse.type_args_constrained -- Parse.binding) --
     2.5          Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
     2.6          Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
     2.7 -    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
     2.8 -        typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
     2.9 +    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy =>
    2.10 +          (if def then
    2.11 +            legacy_feature "typedef with implicit set definition -- use \"typedef (open)\" instead"
    2.12 +           else ();
    2.13 +           typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) lthy)));
    2.14  
    2.15  end;
    2.16