src/HOL/Enum.thy
changeset 59582 0fbed69ff081
parent 58889 5b7a9633cfa8
child 59867 58043346ca64
     1.1 --- a/src/HOL/Enum.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Enum.thy	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -563,12 +563,14 @@
     1.4  by(cases x) simp
     1.5  
     1.6  simproc_setup finite_1_eq ("x::finite_1") = {*
     1.7 -  fn _ => fn _ => fn ct => case term_of ct of
     1.8 -    Const (@{const_name a\<^sub>1}, _) => NONE
     1.9 -  | _ => SOME (mk_meta_eq @{thm finite_1_eq})
    1.10 +  fn _ => fn _ => fn ct =>
    1.11 +    (case Thm.term_of ct of
    1.12 +      Const (@{const_name a\<^sub>1}, _) => NONE
    1.13 +    | _ => SOME (mk_meta_eq @{thm finite_1_eq}))
    1.14  *}
    1.15  
    1.16 -instantiation finite_1 :: complete_boolean_algebra begin
    1.17 +instantiation finite_1 :: complete_boolean_algebra
    1.18 +begin
    1.19  definition [simp]: "op - = (\<lambda>_ _. a\<^sub>1)"
    1.20  definition [simp]: "uminus = (\<lambda>_. a\<^sub>1)"
    1.21  instance by intro_classes simp_all