--- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Aug 19 16:08:54 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Aug 19 16:08:59 2010 +0200
@@ -135,7 +135,7 @@
val thy = Context.theory_of context
val thms_to_be_added = (case (prop_of orig_thm) of
(* case: eqvt-lemma is of the implicational form *)
- (Const("==>", _) $ (Const (@{const_name "Trueprop"},_) $ hyp) $ (Const (@{const_name "Trueprop"},_) $ concl)) =>
+ (Const("==>", _) $ (Const (@{const_name Trueprop},_) $ hyp) $ (Const (@{const_name Trueprop},_) $ concl)) =>
let
val (pi,typi) = get_pi concl thy
in
@@ -147,7 +147,7 @@
else raise EQVT_FORM "Type Implication"
end
(* case: eqvt-lemma is of the equational form *)
- | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
+ | (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $
(Const (@{const_name "perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
(if (apply_pi lhs (pi,typi)) = rhs
then [orig_thm]