# 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;