src/HOL/Ctr_Sugar.thy
changeset 54626 8a5e82425e55
parent 54615 62fb5af93fe2
child 54701 4ed7454aebde
     1.1 --- a/src/HOL/Ctr_Sugar.thy	Mon Dec 02 20:31:54 2013 +0100
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Mon Dec 02 20:31:54 2013 +0100
     1.3 @@ -11,9 +11,7 @@
     1.4  imports HOL
     1.5  keywords
     1.6    "print_case_translations" :: diag and
     1.7 -  "wrap_free_constructors" :: thy_goal and
     1.8 -  "no_discs_sels" and
     1.9 -  "rep_compat"
    1.10 +  "wrap_free_constructors" :: thy_goal
    1.11  begin
    1.12  
    1.13  consts