# HG changeset patch
# User nipkow
# Date 1515256881 -3600
# Node ID 0441f2f1b574e27fa367f7371a5ca67fbcd448a2
# Parent  4c4db8687e50a8a74c8a4c7bc6b40ccbb8dc6d7f
tuned op

diff -r 4c4db8687e50 -r 0441f2f1b574 src/Doc/Locales/Examples2.thy
--- 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