1.1 --- a/src/HOL/Predicate.thy	Tue Apr 21 09:53:31 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Wed Apr 22 11:10:23 2009 +0200
     1.3 @@ -622,6 +622,11 @@
     1.4    "pred_rec f P = f (eval P)"
     1.5    by (cases P) simp
     1.6  
     1.7 +inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
     1.8 +
     1.9 +lemma eq_is_eq: "eq x y \<equiv> (x = y)"
    1.10 +by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
    1.11 +
    1.12  no_notation
    1.13    inf (infixl "\<sqinter>" 70) and
    1.14    sup (infixl "\<squnion>" 65) and
    1.15 @@ -633,6 +638,6 @@
    1.16  
    1.17  hide (open) type pred seq
    1.18  hide (open) const Pred eval single bind if_pred not_pred
    1.19 -  Empty Insert Join Seq member pred_of_seq "apply" adjunct
    1.20 +  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
    1.21  
    1.22  end

     2.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Apr 21 09:53:31 2009 +0200
     2.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Apr 22 11:10:23 2009 +0200
     2.3 @@ -726,15 +726,15 @@
     2.4      Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
     2.5    | _ => error "Trueprop_conv"
     2.6  
     2.7 -fun preprocess_intro thy rule = Thm.transfer thy rule (*FIXME preprocessor
     2.8 +fun preprocess_intro thy rule =
     2.9    Conv.fconv_rule
    2.10      (imp_prems_conv
    2.11 -      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @ {thm Predicate.eq_is_eq})))))
    2.12 -    (Thm.transfer thy rule) *)
    2.13 +      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
    2.14 +    (Thm.transfer thy rule)
    2.15  
    2.16 -fun preprocess_elim thy nargs elimrule = (*FIXME preprocessor -- let
    2.17 +fun preprocess_elim thy nargs elimrule = let
    2.18     fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
    2.19 -      HOLogic.mk_Trueprop (Const (@ {const_name Predicate.eq}, T) $ lhs $ rhs)
    2.20 +      HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
    2.21      | replace_eqs t = t
    2.22     fun preprocess_case t = let
    2.23       val params = Logic.strip_params t
    2.24 @@ -746,10 +746,10 @@
    2.25     val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
    2.26   in
    2.27     Thm.equal_elim
    2.28 -     (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@ {thm eq_is_eq}])
    2.29 +     (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}])
    2.30          (cterm_of thy elimrule')))
    2.31       elimrule
    2.32 - end*) elimrule;
    2.33 + end;
    2.34  
    2.35  
    2.36  (* returns true if t is an application of an datatype constructor *)