--- a/src/HOL/Library/conditional_parametricity.ML Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Library/conditional_parametricity.ML Wed Jan 10 15:25:09 2018 +0100
@@ -390,7 +390,7 @@
Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t;
val is_equality_lemma =
- @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
+ @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (=))"
by (unfold is_equality_def, rule, drule meta_spec,
erule meta_mp, rule HOL.refl, simp)};
@@ -398,7 +398,7 @@
let
val prop = Thm.prop_of thm
val (t, mk_prop') = dest prop
- (* Only consider "op =" at non-base types *)
+ (* Only consider "(=)" at non-base types *)
fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
(case T of Type (_, []) => false | _ => true)
| is_eq _ = false
@@ -516,4 +516,4 @@
Outer_Syntax.local_theory @{command_keyword parametric_constant} "proves parametricity"
((Parse_Spec.opt_thm_name ":" -- Parse.thm) >> parametric_constant_cmd);
-end;
\ No newline at end of file
+end;