# HG changeset patch
# User wenzelm
# Date 1672950829 -3600
# Node ID 8a66a88cd5dced991a83cd725e50d3deaf8105d6
# Parent  aea34e2cabe8cf3440bbe11c7ef83a27fe65d230
isabelle update -u path_cartouches;

diff -r aea34e2cabe8 -r 8a66a88cd5dc src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Jan 05 21:18:55 2023 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Jan 05 21:33:49 2023 +0100
@@ -1324,8 +1324,8 @@
   files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into a temporary
   directory, which is taken as starting point for build process of
   Isabelle/Scala/Java modules (see @{cite "isabelle-system"}). The
-  corresponding @{path build.props} file is expected directly in the toplevel
-  directory, instead of @{path "etc/build.props"} for Isabelle system
+  corresponding @{path \<open>build.props\<close>} file is expected directly in the toplevel
+  directory, instead of @{path \<open>etc/build.props\<close>} for Isabelle system
   components. These properties need to specify sources, resources, services
   etc. as usual. The resulting JAR module becomes an export artefact of the
   session database, with a name of the form
diff -r aea34e2cabe8 -r 8a66a88cd5dc src/HOL/Analysis/Metric_Arith.thy
--- a/src/HOL/Analysis/Metric_Arith.thy	Thu Jan 05 21:18:55 2023 +0100
+++ b/src/HOL/Analysis/Metric_Arith.thy	Thu Jan 05 21:33:49 2023 +0100
@@ -105,7 +105,7 @@
   "x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x = y \<longleftrightarrow> (\<forall>a\<in>s. dist x a = dist y a)"
   by auto
 
-ML_file "metric_arith.ML"
+ML_file \<open>metric_arith.ML\<close>
 
 method_setup metric = \<open>
   Scan.succeed (SIMPLE_METHOD' o Metric_Arith.metric_arith_tac)
diff -r aea34e2cabe8 -r 8a66a88cd5dc src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Jan 05 21:18:55 2023 +0100
+++ b/src/HOL/Quotient.thy	Thu Jan 05 21:33:49 2023 +0100
@@ -870,7 +870,7 @@
   unfolding Quotient_def eq_onp_def
   by unfold_locales auto
 
-ML_file "Tools/BNF/bnf_lift.ML"
+ML_file \<open>Tools/BNF/bnf_lift.ML\<close>
 
 hide_fact
   sum_insert_Inl_unit lift_sum_unit_vimage_commute insert_Inl_int_map_sum_unit
diff -r aea34e2cabe8 -r 8a66a88cd5dc src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Jan 05 21:18:55 2023 +0100
+++ b/src/Pure/Pure.thy	Thu Jan 05 21:33:49 2023 +0100
@@ -202,8 +202,8 @@
               (Toplevel.context_of st) args external)));
 in end\<close>
 
-external_file "ROOT0.ML"
-external_file "ROOT.ML"
+external_file \<open>ROOT0.ML\<close>
+external_file \<open>ROOT.ML\<close>
 
 
 subsection \<open>Embedded ML text\<close>