src/Doc/Locales/Examples2.thy
changeset 67349 0441f2f1b574
parent 61566 c3d6e570ccef
child 67399 eab6ce8368fa
--- a/src/Doc/Locales/Examples2.thy	Sat Jan 06 17:39:32 2018 +0100
+++ b/src/Doc/Locales/Examples2.thy	Sat Jan 06 17:41:21 2018 +0100
@@ -12,7 +12,7 @@
     txt \<open>\normalsize The second goal is shown by unfolding the
       definition of @{term "partial_order.less"}.\<close>
     show "partial_order.less op \<le> x y = (x < y)"
-      unfolding partial_order.less_def [OF \<open>partial_order op \<le>\<close>]
+      unfolding partial_order.less_def [OF \<open>partial_order (op \<le>)\<close>]
       by auto
   qed