src/HOL/Enum.thy
changeset 52435 6646bb548c6b
parent 50567 768a3fbe4149
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Enum.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/Enum.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -117,7 +117,9 @@
     1.4  qed
     1.5  
     1.6  code_abort enum_the
     1.7 -code_const enum_the (Eval "(fn p => raise Match)")
     1.8 +
     1.9 +code_printing
    1.10 +  constant enum_the \<rightharpoonup> (Eval) "(fn '_ => raise Match)"
    1.11  
    1.12  
    1.13  subsubsection {* Equality and order on functions *}