--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Thu Feb 15 12:11:00 2018 +0100
@@ -91,7 +91,7 @@
(******************************************************************************)
val case_UU_allI =
- @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}
+ @{lemma "(\<And>x. x \<noteq> UU \<Longrightarrow> P x) \<Longrightarrow> P UU \<Longrightarrow> \<forall>x. P x" by metis}
fun prove_induction
(comp_dbind : binding)