# HG changeset patch
# User wenzelm
# Date 1546783873 -3600
# Node ID 157990515be16dcb272fa6f1f0c3caa8034a9857
# Parent  86e8e7347ac00fcfb7e01f4b0fa779824697bc69# Parent  a963200742980f3bd9e613dafc3b54b127ddfc62
merged

diff -r 86e8e7347ac0 -r 157990515be1 etc/options
--- a/etc/options	Sun Jan 06 12:32:01 2019 +0100
+++ b/etc/options	Sun Jan 06 15:11:13 2019 +0100
@@ -288,6 +288,9 @@
 option update_control_cartouches : bool = false
   -- "update antiquotations to use control symbol with cartouche argument"
 
+option update_path_cartouches : bool = false
+  -- "update file-system paths to use cartouches"
+
 
 section "Build Database"
 
diff -r 86e8e7347ac0 -r 157990515be1 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/CTT/CTT.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,7 +9,7 @@
 
 section \<open>Constructive Type Theory: axiomatic basis\<close>
 
-ML_file "~~/src/Provers/typedsimp.ML"
+ML_file \<open>~~/src/Provers/typedsimp.ML\<close>
 setup Pure_Thy.old_appl_syntax_setup
 
 typedecl i
@@ -455,7 +455,7 @@
 method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close>
 method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close>
 
-ML_file "rew.ML"
+ML_file \<open>rew.ML\<close>
 method_setup rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths))\<close>
 method_setup hyp_rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths))\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Classes/Setup.thy
--- a/src/Doc/Classes/Setup.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Classes/Setup.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -2,8 +2,8 @@
 imports Main
 begin
 
-ML_file "../antiquote_setup.ML"
-ML_file "../more_antiquote.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
+ML_file \<open>../more_antiquote.ML\<close>
 
 declare [[default_code_width = 74]]
 
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Codegen/Introduction.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -69,7 +69,7 @@
 text \<open>\noindent Then we can generate code e.g.~for \<open>SML\<close> as follows:\<close>
 
 export_code %quote empty dequeue enqueue in SML
-  module_name Example file "$ISABELLE_TMP/example.ML"
+  module_name Example file \<open>$ISABELLE_TMP/example.ML\<close>
 
 text \<open>\noindent resulting in the following code:\<close>
 
@@ -90,7 +90,7 @@
 \<close>
 
 export_code %quote empty dequeue enqueue in Haskell
-  module_name Example file "$ISABELLE_TMP/examples/"
+  module_name Example file \<open>$ISABELLE_TMP/examples/\<close>
 
 text \<open>
   \noindent This is the corresponding code:
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Codegen/Setup.thy
--- a/src/Doc/Codegen/Setup.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Codegen/Setup.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -7,8 +7,8 @@
   "HOL-Library.IArray"
 begin
 
-ML_file "../antiquote_setup.ML"
-ML_file "../more_antiquote.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
+ML_file \<open>../more_antiquote.ML\<close>
 
 no_syntax (output)
   "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Datatypes/Setup.thy
--- a/src/Doc/Datatypes/Setup.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Datatypes/Setup.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -2,6 +2,6 @@
 imports Main
 begin
 
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Eisbach/Base.thy
--- a/src/Doc/Eisbach/Base.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Eisbach/Base.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -6,7 +6,7 @@
 imports Main
 begin
 
-ML_file "~~/src/Doc/antiquote_setup.ML"
+ML_file \<open>~~/src/Doc/antiquote_setup.ML\<close>
 
 ML\<open>
 fun get_split_rule ctxt target =
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Implementation/Base.thy
--- a/src/Doc/Implementation/Base.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Implementation/Base.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -4,6 +4,6 @@
 imports Main
 begin
 
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Isar_Ref/Base.thy
--- a/src/Doc/Isar_Ref/Base.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Isar_Ref/Base.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -4,6 +4,6 @@
 imports Pure
 begin
 
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/JEdit/Base.thy
--- a/src/Doc/JEdit/Base.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/JEdit/Base.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -4,6 +4,6 @@
 imports Main
 begin
 
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Logics_ZF/ZF_Isar.thy
--- a/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -3,7 +3,7 @@
 begin
 
 (*<*)
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
 (*>*)
 
 chapter \<open>Some Isar language elements\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/System/Base.thy
--- a/src/Doc/System/Base.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/System/Base.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -4,6 +4,6 @@
 imports Pure
 begin
 
-ML_file "../antiquote_setup.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -734,16 +734,18 @@
     example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by
     ``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.)
 
+    \<^item> @{system_option update_path_cartouches} to update file-system paths to
+    use cartouches: this depends on language markup provided by semantic
+    processing of parsed input.
+
   It is also possible to produce custom updates in Isabelle/ML, by reporting
   \<^ML>\<open>Markup.update\<close> with the precise source position and a replacement
   text. This operation should be made conditional on specific system options,
   similar to the ones above. Searching the above option names in ML sources of
   \<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples.
 
-  Different update options can be in conflict by producing overlapping edits:
-  this may require to run @{tool update} multiple times, but it is often
-  better to enable particular update options separately and commit the changes
-  one-by-one.
+  Updates can be in conflict by producing nested or overlapping edits: this
+  may require to run @{tool update} multiple times.
 \<close>
 
 
@@ -769,7 +771,7 @@
   separately with special options as follows:
 
   @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs
-  -o record_proofs=2 -o parallel_proofs=0\<close>}
+  -o record_proofs=2\<close>}
 
   \<^smallskip> See also the end of \secref{sec:tool-dump} for hints on increasing
   Isabelle/ML heap sizes for very big PIDE processes that include many
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Tutorial/Inductive/Advanced.thy
--- a/src/Doc/Tutorial/Inductive/Advanced.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Tutorial/Inductive/Advanced.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -1,5 +1,5 @@
 (*<*)theory Advanced imports Even begin
-ML_file "../../antiquote_setup.ML"
+ML_file \<open>../../antiquote_setup.ML\<close>
 (*>*)
 
 text \<open>
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Tutorial/Inductive/Even.thy
--- a/src/Doc/Tutorial/Inductive/Even.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Tutorial/Inductive/Even.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -1,5 +1,5 @@
 (*<*)theory Even imports Main begin
-ML_file "../../antiquote_setup.ML" 
+ML_file \<open>../../antiquote_setup.ML\<close> 
 (*>*)
 
 section\<open>The Set of Even Numbers\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 section\<open>Theory of Agents and Messages for Security Protocols\<close>
 
 theory Message imports Main begin
-ML_file "../../antiquote_setup.ML"
+ML_file \<open>../../antiquote_setup.ML\<close>
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Tutorial/Types/Setup.thy
--- a/src/Doc/Tutorial/Types/Setup.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Tutorial/Types/Setup.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -2,7 +2,7 @@
 imports Main
 begin
 
-ML_file "../../antiquote_setup.ML"
-ML_file "../../more_antiquote.ML"
+ML_file \<open>../../antiquote_setup.ML\<close>
+ML_file \<open>../../more_antiquote.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/Doc/Typeclass_Hierarchy/Setup.thy
--- a/src/Doc/Typeclass_Hierarchy/Setup.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -2,8 +2,8 @@
 imports Complex_Main "HOL-Library.Multiset" "HOL-Library.Lattice_Syntax"
 begin
 
-ML_file "../antiquote_setup.ML"
-ML_file "../more_antiquote.ML"
+ML_file \<open>../antiquote_setup.ML\<close>
+ML_file \<open>../more_antiquote.ML\<close>
 
 attribute_setup all =
   \<open>Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/FOL/FOL.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,9 +9,9 @@
 keywords "print_claset" "print_induct_rules" :: diag
 begin
 
-ML_file "~~/src/Provers/classical.ML"
-ML_file "~~/src/Provers/blast.ML"
-ML_file "~~/src/Provers/clasimp.ML"
+ML_file \<open>~~/src/Provers/classical.ML\<close>
+ML_file \<open>~~/src/Provers/blast.ML\<close>
+ML_file \<open>~~/src/Provers/clasimp.ML\<close>
 
 
 subsection \<open>The classical axiom\<close>
@@ -335,7 +335,7 @@
   not_imp not_all not_ex cases_simp cla_simps_misc
 
 
-ML_file "simpdata.ML"
+ML_file \<open>simpdata.ML\<close>
 
 simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_ex\<close>
 simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_all\<close>
@@ -361,7 +361,7 @@
   Simplifier.method_setup Splitter.split_modifiers
 \<close>
 
-ML_file "~~/src/Tools/eqsubst.ML"
+ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
 
 
 subsection \<open>Other simple lemmas\<close>
@@ -429,7 +429,7 @@
 
 text \<open>Method setup.\<close>
 
-ML_file "~~/src/Tools/induct.ML"
+ML_file \<open>~~/src/Tools/induct.ML\<close>
 ML \<open>
   structure Induct = Induct
   (
@@ -447,7 +447,7 @@
 
 end
 
-ML_file "~~/src/Tools/case_product.ML"
+ML_file \<open>~~/src/Tools/case_product.ML\<close>
 
 
 hide_const (open) eq
diff -r 86e8e7347ac0 -r 157990515be1 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/FOL/IFOL.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,16 +9,16 @@
 begin
 
 ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
-ML_file "~~/src/Tools/misc_legacy.ML"
-ML_file "~~/src/Provers/splitter.ML"
-ML_file "~~/src/Provers/hypsubst.ML"
-ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
-ML_file "~~/src/Tools/IsaPlanner/isand.ML"
-ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
-ML_file "~~/src/Provers/quantifier1.ML"
-ML_file "~~/src/Tools/intuitionistic.ML"
-ML_file "~~/src/Tools/project_rule.ML"
-ML_file "~~/src/Tools/atomize_elim.ML"
+ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
+ML_file \<open>~~/src/Provers/splitter.ML\<close>
+ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
+ML_file \<open>~~/src/Provers/quantifier1.ML\<close>
+ML_file \<open>~~/src/Tools/intuitionistic.ML\<close>
+ML_file \<open>~~/src/Tools/project_rule.ML\<close>
+ML_file \<open>~~/src/Tools/atomize_elim.ML\<close>
 
 
 subsection \<open>Syntax and axiomatic basis\<close>
@@ -582,7 +582,7 @@
 )
 \<close>
 
-ML_file "fologic.ML"
+ML_file \<open>fologic.ML\<close>
 
 lemma thin_refl: \<open>\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W\<close> .
 
@@ -603,7 +603,7 @@
 open Hypsubst;
 \<close>
 
-ML_file "intprover.ML"
+ML_file \<open>intprover.ML\<close>
 
 
 subsection \<open>Intuitionistic Reasoning\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/FOLP/FOLP.thy
--- a/src/FOLP/FOLP.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/FOLP/FOLP.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -98,8 +98,8 @@
   apply assumption
   done
 
-ML_file "classical.ML"      (* Patched because matching won't instantiate proof *)
-ML_file "simp.ML"           (* Patched because matching won't instantiate proof *)
+ML_file \<open>classical.ML\<close>      (* Patched because matching won't instantiate proof *)
+ML_file \<open>simp.ML\<close>           (* Patched because matching won't instantiate proof *)
 
 ML \<open>
 structure Cla = Classical
@@ -138,6 +138,6 @@
   apply (tactic \<open>ALLGOALS (Cla.fast_tac \<^context> FOLP_cs)\<close>)
   done
 
-ML_file "simpdata.ML"
+ML_file \<open>simpdata.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/FOLP/IFOLP.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,7 +9,7 @@
 imports Pure
 begin
 
-ML_file "~~/src/Tools/misc_legacy.ML"
+ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
 
 setup Pure_Thy.old_appl_syntax_setup
 
@@ -605,7 +605,7 @@
 
 lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
 
-ML_file "hypsubst.ML"
+ML_file \<open>hypsubst.ML\<close>
 
 ML \<open>
 structure Hypsubst = Hypsubst
@@ -627,7 +627,7 @@
 open Hypsubst;
 \<close>
 
-ML_file "intprover.ML"
+ML_file \<open>intprover.ML\<close>
 
 
 (*** Rewrite rules ***)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/ATP.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -11,11 +11,11 @@
 
 subsection \<open>ATP problems and proofs\<close>
 
-ML_file "Tools/ATP/atp_util.ML"
-ML_file "Tools/ATP/atp_problem.ML"
-ML_file "Tools/ATP/atp_proof.ML"
-ML_file "Tools/ATP/atp_proof_redirect.ML"
-ML_file "Tools/ATP/atp_satallax.ML"
+ML_file \<open>Tools/ATP/atp_util.ML\<close>
+ML_file \<open>Tools/ATP/atp_problem.ML\<close>
+ML_file \<open>Tools/ATP/atp_proof.ML\<close>
+ML_file \<open>Tools/ATP/atp_proof_redirect.ML\<close>
+ML_file \<open>Tools/ATP/atp_satallax.ML\<close>
 
 
 subsection \<open>Higher-order reasoning helpers\<close>
@@ -146,12 +146,12 @@
 
 subsection \<open>Basic connection between ATPs and HOL\<close>
 
-ML_file "Tools/lambda_lifting.ML"
-ML_file "Tools/monomorph.ML"
-ML_file "Tools/ATP/atp_problem_generate.ML"
-ML_file "Tools/ATP/atp_proof_reconstruct.ML"
-ML_file "Tools/ATP/atp_systems.ML"
-ML_file "Tools/ATP/atp_waldmeister.ML"
+ML_file \<open>Tools/lambda_lifting.ML\<close>
+ML_file \<open>Tools/monomorph.ML\<close>
+ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
+ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
+ML_file \<open>Tools/ATP/atp_waldmeister.ML\<close>
 
 hide_fact (open) waldmeister_fol boolean_equality boolean_comm
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Algebra/Ring.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -418,7 +418,7 @@
   compute distributive normal form in locale contexts\<close>
 
 
-ML_file "ringsimp.ML"
+ML_file \<open>ringsimp.ML\<close>
 
 attribute_setup algebra = \<open>
   Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || Scan.succeed true)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Analysis/Measurable.thy
--- a/src/HOL/Analysis/Measurable.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Analysis/Measurable.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -46,7 +46,7 @@
 lemma pred_sets2: "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> pred M (\<lambda>x. f x \<in> A)"
   by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])
 
-ML_file "measurable.ML"
+ML_file \<open>measurable.ML\<close>
 
 attribute_setup measurable = \<open>
   Scan.lift (
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Analysis/Norm_Arith.thy
--- a/src/HOL/Analysis/Norm_Arith.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Analysis/Norm_Arith.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -129,7 +129,7 @@
   mult_1_left
   mult_1_right
 
-ML_file "normarith.ML"
+ML_file \<open>normarith.ML\<close>
 
 method_setup%important norm = \<open>
   Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Argo.thy
--- a/src/HOL/Argo.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Argo.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -6,22 +6,22 @@
 imports HOL
 begin
 
-ML_file "~~/src/Tools/Argo/argo_expr.ML"
-ML_file "~~/src/Tools/Argo/argo_term.ML"
-ML_file "~~/src/Tools/Argo/argo_lit.ML"
-ML_file "~~/src/Tools/Argo/argo_proof.ML"
-ML_file "~~/src/Tools/Argo/argo_rewr.ML"
-ML_file "~~/src/Tools/Argo/argo_cls.ML"
-ML_file "~~/src/Tools/Argo/argo_common.ML"
-ML_file "~~/src/Tools/Argo/argo_cc.ML"
-ML_file "~~/src/Tools/Argo/argo_simplex.ML"
-ML_file "~~/src/Tools/Argo/argo_thy.ML"
-ML_file "~~/src/Tools/Argo/argo_heap.ML"
-ML_file "~~/src/Tools/Argo/argo_cdcl.ML"
-ML_file "~~/src/Tools/Argo/argo_core.ML"
-ML_file "~~/src/Tools/Argo/argo_clausify.ML"
-ML_file "~~/src/Tools/Argo/argo_solver.ML"
+ML_file \<open>~~/src/Tools/Argo/argo_expr.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_term.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_lit.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_proof.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_rewr.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_cls.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_common.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_cc.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_simplex.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_thy.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_heap.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_cdcl.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_core.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_clausify.ML\<close>
+ML_file \<open>~~/src/Tools/Argo/argo_solver.ML\<close>
 
-ML_file "Tools/Argo/argo_tactic.ML"
+ML_file \<open>Tools/Argo/argo_tactic.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/BNF_Composition.thy
--- a/src/HOL/BNF_Composition.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Composition.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -178,9 +178,9 @@
 lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV"
   unfolding id_bnf_def by unfold_locales auto
 
-ML_file "Tools/BNF/bnf_comp_tactics.ML"
-ML_file "Tools/BNF/bnf_comp.ML"
-ML_file "Tools/BNF/bnf_lift.ML"
+ML_file \<open>Tools/BNF/bnf_comp_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_comp.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lift.ML\<close>
 
 hide_fact
   DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Def.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -272,9 +272,9 @@
 lemma eq_onp_mono_iff: "eq_onp P \<le> eq_onp Q \<longleftrightarrow> P \<le> Q"
   unfolding eq_onp_def by auto
 
-ML_file "Tools/BNF/bnf_util.ML"
-ML_file "Tools/BNF/bnf_tactics.ML"
-ML_file "Tools/BNF/bnf_def_tactics.ML"
-ML_file "Tools/BNF/bnf_def.ML"
+ML_file \<open>Tools/BNF/bnf_util.ML\<close>
+ML_file \<open>Tools/BNF/bnf_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_def_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_def.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/BNF_Fixpoint_Base.thy
--- a/src/HOL/BNF_Fixpoint_Base.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -287,12 +287,12 @@
 lemma Let_const: "Let x (\<lambda>_. c) = c"
   unfolding Let_def ..
 
-ML_file "Tools/BNF/bnf_fp_util_tactics.ML"
-ML_file "Tools/BNF/bnf_fp_util.ML"
-ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
-ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
-ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
-ML_file "Tools/BNF/bnf_fp_n2m.ML"
-ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
+ML_file \<open>Tools/BNF/bnf_fp_util_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_util.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_def_sugar_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_def_sugar.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_n2m_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_n2m.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_n2m_sugar.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/BNF_Greatest_Fixpoint.thy
--- a/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -281,10 +281,10 @@
   thus "univ f X \<in> B" using x PRES by simp
 qed
 
-ML_file "Tools/BNF/bnf_gfp_util.ML"
-ML_file "Tools/BNF/bnf_gfp_tactics.ML"
-ML_file "Tools/BNF/bnf_gfp.ML"
-ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
-ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
+ML_file \<open>Tools/BNF/bnf_gfp_util.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_gfp_rec_sugar.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -196,11 +196,11 @@
 lemma pred_fun_True_id: "NO_MATCH id p \<Longrightarrow> pred_fun (\<lambda>x. True) p f = pred_fun (\<lambda>x. True) id (p \<circ> f)"
   unfolding fun.pred_map unfolding comp_def id_def ..
 
-ML_file "Tools/BNF/bnf_lfp_util.ML"
-ML_file "Tools/BNF/bnf_lfp_tactics.ML"
-ML_file "Tools/BNF/bnf_lfp.ML"
-ML_file "Tools/BNF/bnf_lfp_compat.ML"
-ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
-ML_file "Tools/BNF/bnf_lfp_size.ML"
+ML_file \<open>Tools/BNF/bnf_lfp_util.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_tactics.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_compat.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar_more.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_size.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Basic_BNF_LFPs.thy
--- a/src/HOL/Basic_BNF_LFPs.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Basic_BNF_LFPs.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -102,7 +102,7 @@
 lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \<and> R2 (snd p) (snd q))"
   by (force simp: rel_prod.simps elim: rel_prod.cases)
 
-ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
+ML_file \<open>Tools/BNF/bnf_lfp_basic_sugar.ML\<close>
 
 declare prod.size [no_atp]
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Code_Evaluation.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -94,11 +94,11 @@
 | constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
 | constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
 
-ML_file "Tools/code_evaluation.ML"
+ML_file \<open>Tools/code_evaluation.ML\<close>
 
 code_reserved Eval Code_Evaluation
 
-ML_file "~~/src/HOL/Tools/value_command.ML"
+ML_file \<open>~~/src/HOL/Tools/value_command.ML\<close>
 
 
 subsection \<open>Dedicated \<open>term_of\<close> instances\<close>
@@ -141,7 +141,7 @@
 
 subsection \<open>Generic reification\<close>
 
-ML_file "~~/src/HOL/Tools/reification.ML"
+ML_file \<open>~~/src/HOL/Tools/reification.ML\<close>
 
 
 subsection \<open>Diagnostic\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Ctr_Sugar.thy
--- a/src/HOL/Ctr_Sugar.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Ctr_Sugar.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -27,7 +27,7 @@
 declare [[coercion_args case_abs -]]
 declare [[coercion_args case_elem - +]]
 
-ML_file "Tools/Ctr_Sugar/case_translation.ML"
+ML_file \<open>Tools/Ctr_Sugar/case_translation.ML\<close>
 
 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
   by (erule iffI) (erule contrapos_pn)
@@ -37,13 +37,13 @@
   "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
   by blast+
 
-ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
-ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
-ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
-ML_file "Tools/Ctr_Sugar/ctr_sugar.ML"
+ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_util.ML\<close>
+ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_tactics.ML\<close>
+ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_code.ML\<close>
+ML_file \<open>Tools/Ctr_Sugar/ctr_sugar.ML\<close>
 
 text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close>
 
-ML_file "Tools/coinduction.ML"
+ML_file \<open>Tools/coinduction.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -1635,7 +1635,7 @@
   "n \<in> {m .. l} \<longleftrightarrow> real n \<in> {real m .. real l}"
   by (simp_all add: real_div_nat_eq_floor_of_divide minus_div_mult_eq_mod [symmetric])
 
-ML_file "approximation.ML"
+ML_file \<open>approximation.ML\<close>
 
 method_setup approximation = \<open>
   let
@@ -1667,7 +1667,7 @@
     "\<not> \<not> q \<longleftrightarrow> q"
   by auto
 
-ML_file "approximation_generator.ML"
+ML_file \<open>approximation_generator.ML\<close>
 setup "Approximation_Generator.setup"
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -2527,7 +2527,7 @@
 end
 \<close>
 
-ML_file "cooper_tac.ML"
+ML_file \<open>cooper_tac.ML\<close>
 
 method_setup cooper = \<open>
   Scan.lift (Args.mode "no_quantify") >>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,8 +9,8 @@
 imports Main
 begin
 
-ML_file "langford_data.ML"
-ML_file "ferrante_rackoff_data.ML"
+ML_file \<open>langford_data.ML\<close>
+ML_file \<open>ferrante_rackoff_data.ML\<close>
 
 context linorder
 begin
@@ -424,7 +424,7 @@
 
 lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
 
-ML_file "langford.ML"
+ML_file \<open>langford.ML\<close>
 method_setup dlo = \<open>
   Scan.succeed (SIMPLE_METHOD' o Langford.dlo_tac)
 \<close> "Langford's algorithm for quantifier elimination in dense linear orders"
@@ -746,7 +746,7 @@
 
 end
 
-ML_file "ferrante_rackoff.ML"
+ML_file \<open>ferrante_rackoff.ML\<close>
 
 method_setup ferrack = \<open>
   Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -2546,7 +2546,7 @@
 end
 \<close>
 
-ML_file "ferrack_tac.ML"
+ML_file \<open>ferrack_tac.ML\<close>
 
 method_setup rferrack = \<open>
   Scan.lift (Args.mode "no_quantify") >>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -5696,7 +5696,7 @@
                          of_int_less_iff [where 'a = real, symmetric]
                          of_int_le_iff [where 'a = real, symmetric]
 
-ML_file "mir_tac.ML"
+ML_file \<open>mir_tac.ML\<close>
 
 method_setup mir = \<open>
   Scan.lift (Args.mode "no_quantify") >>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Eisbach/Eisbach.thy
--- a/src/HOL/Eisbach/Eisbach.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Eisbach/Eisbach.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -15,10 +15,10 @@
   "uses"
 begin
 
-ML_file "parse_tools.ML"
-ML_file "method_closure.ML"
-ML_file "eisbach_rule_insts.ML"
-ML_file "match_method.ML"
+ML_file \<open>parse_tools.ML\<close>
+ML_file \<open>method_closure.ML\<close>
+ML_file \<open>eisbach_rule_insts.ML\<close>
+ML_file \<open>match_method.ML\<close>
 
 
 method solves methods m = (m; fail)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Extraction.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports Option
 begin
 
-ML_file "Tools/rewrite_hol_proof.ML"
+ML_file \<open>Tools/rewrite_hol_proof.ML\<close>
 
 subsection \<open>Setup\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Fields.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -57,8 +57,8 @@
 
 text \<open>Setup for linear arithmetic prover\<close>
 
-ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
-ML_file "Tools/lin_arith.ML"
+ML_file \<open>~~/src/Provers/Arith/fast_lin_arith.ML\<close>
+ML_file \<open>Tools/lin_arith.ML\<close>
 setup \<open>Lin_Arith.global_setup\<close>
 declaration \<open>K Lin_Arith.setup\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Fun.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -886,7 +886,7 @@
 
 subsubsection \<open>Functorial structure of types\<close>
 
-ML_file "Tools/functor.ML"
+ML_file \<open>Tools/functor.ML\<close>
 
 functor map_fun: map_fun
   by (simp_all add: fun_eq_iff)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Fun_Def.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -77,25 +77,25 @@
 lemma wf_in_rel: "wf R \<Longrightarrow> wfP (in_rel R)"
   by (simp add: wfP_def)
 
-ML_file "Tools/Function/function_core.ML"
-ML_file "Tools/Function/mutual.ML"
-ML_file "Tools/Function/pattern_split.ML"
-ML_file "Tools/Function/relation.ML"
-ML_file "Tools/Function/function_elims.ML"
+ML_file \<open>Tools/Function/function_core.ML\<close>
+ML_file \<open>Tools/Function/mutual.ML\<close>
+ML_file \<open>Tools/Function/pattern_split.ML\<close>
+ML_file \<open>Tools/Function/relation.ML\<close>
+ML_file \<open>Tools/Function/function_elims.ML\<close>
 
 method_setup relation = \<open>
   Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
 \<close> "prove termination using a user-specified wellfounded relation"
 
-ML_file "Tools/Function/function.ML"
-ML_file "Tools/Function/pat_completeness.ML"
+ML_file \<open>Tools/Function/function.ML\<close>
+ML_file \<open>Tools/Function/pat_completeness.ML\<close>
 
 method_setup pat_completeness = \<open>
   Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
 \<close> "prove completeness of (co)datatype patterns"
 
-ML_file "Tools/Function/fun.ML"
-ML_file "Tools/Function/induction_schema.ML"
+ML_file \<open>Tools/Function/fun.ML\<close>
+ML_file \<open>Tools/Function/induction_schema.ML\<close>
 
 method_setup induction_schema = \<open>
   Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac)
@@ -108,7 +108,7 @@
   where is_measure_trivial: "is_measure f"
 
 named_theorems measure_function "rules that guide the heuristic generation of measure functions"
-ML_file "Tools/Function/measure_functions.ML"
+ML_file \<open>Tools/Function/measure_functions.ML\<close>
 
 lemma measure_size[measure_function]: "is_measure size"
   by (rule is_measure_trivial)
@@ -119,7 +119,7 @@
 lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
   by (rule is_measure_trivial)
 
-ML_file "Tools/Function/lexicographic_order.ML"
+ML_file \<open>Tools/Function/lexicographic_order.ML\<close>
 
 method_setup lexicographic_order = \<open>
   Method.sections clasimp_modifiers >>
@@ -290,10 +290,10 @@
 
 subsection \<open>Tool setup\<close>
 
-ML_file "Tools/Function/termination.ML"
-ML_file "Tools/Function/scnp_solve.ML"
-ML_file "Tools/Function/scnp_reconstruct.ML"
-ML_file "Tools/Function/fun_cases.ML"
+ML_file \<open>Tools/Function/termination.ML\<close>
+ML_file \<open>Tools/Function/scnp_solve.ML\<close>
+ML_file \<open>Tools/Function/scnp_reconstruct.ML\<close>
+ML_file \<open>Tools/Function/fun_cases.ML\<close>
 
 ML_val \<comment> \<open>setup inactive\<close>
 \<open>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Fun_Def_Base.thy
--- a/src/HOL/Fun_Def_Base.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Fun_Def_Base.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,15 +8,15 @@
 imports Ctr_Sugar Set Wellfounded
 begin
 
-ML_file "Tools/Function/function_lib.ML"
+ML_file \<open>Tools/Function/function_lib.ML\<close>
 named_theorems termination_simp "simplification rules for termination proofs"
-ML_file "Tools/Function/function_common.ML"
-ML_file "Tools/Function/function_context_tree.ML"
+ML_file \<open>Tools/Function/function_common.ML\<close>
+ML_file \<open>Tools/Function/function_context_tree.ML\<close>
 
 attribute_setup fundef_cong =
   \<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close>
   "declaration of congruence rule for function definitions"
 
-ML_file "Tools/Function/sum_tree.ML"
+ML_file \<open>Tools/Function/sum_tree.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Groebner_Basis.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -33,7 +33,7 @@
   by auto
 
 named_theorems algebra "pre-simplification rules for algebraic methods"
-ML_file "Tools/groebner.ML"
+ML_file \<open>Tools/groebner.ML\<close>
 
 method_setup algebra = \<open>
   let
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Groups.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -988,7 +988,7 @@
 
 end
 
-ML_file "Tools/group_cancel.ML"
+ML_file \<open>Tools/group_cancel.ML\<close>
 
 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
   \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOL.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -12,26 +12,26 @@
   "quickcheck_params" :: thy_decl
 begin
 
-ML_file "~~/src/Tools/misc_legacy.ML"
-ML_file "~~/src/Tools/try.ML"
-ML_file "~~/src/Tools/quickcheck.ML"
-ML_file "~~/src/Tools/solve_direct.ML"
-ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
-ML_file "~~/src/Tools/IsaPlanner/isand.ML"
-ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
-ML_file "~~/src/Provers/hypsubst.ML"
-ML_file "~~/src/Provers/splitter.ML"
-ML_file "~~/src/Provers/classical.ML"
-ML_file "~~/src/Provers/blast.ML"
-ML_file "~~/src/Provers/clasimp.ML"
-ML_file "~~/src/Tools/eqsubst.ML"
-ML_file "~~/src/Provers/quantifier1.ML"
-ML_file "~~/src/Tools/atomize_elim.ML"
-ML_file "~~/src/Tools/cong_tac.ML"
-ML_file "~~/src/Tools/intuitionistic.ML" setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
-ML_file "~~/src/Tools/project_rule.ML"
-ML_file "~~/src/Tools/subtyping.ML"
-ML_file "~~/src/Tools/case_product.ML"
+ML_file \<open>~~/src/Tools/misc_legacy.ML\<close>
+ML_file \<open>~~/src/Tools/try.ML\<close>
+ML_file \<open>~~/src/Tools/quickcheck.ML\<close>
+ML_file \<open>~~/src/Tools/solve_direct.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close>
+ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close>
+ML_file \<open>~~/src/Provers/hypsubst.ML\<close>
+ML_file \<open>~~/src/Provers/splitter.ML\<close>
+ML_file \<open>~~/src/Provers/classical.ML\<close>
+ML_file \<open>~~/src/Provers/blast.ML\<close>
+ML_file \<open>~~/src/Provers/clasimp.ML\<close>
+ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
+ML_file \<open>~~/src/Provers/quantifier1.ML\<close>
+ML_file \<open>~~/src/Tools/atomize_elim.ML\<close>
+ML_file \<open>~~/src/Tools/cong_tac.ML\<close>
+ML_file \<open>~~/src/Tools/intuitionistic.ML\<close> setup \<open>Intuitionistic.method_setup \<^binding>\<open>iprover\<close>\<close>
+ML_file \<open>~~/src/Tools/project_rule.ML\<close>
+ML_file \<open>~~/src/Tools/subtyping.ML\<close>
+ML_file \<open>~~/src/Tools/case_product.ML\<close>
 
 
 ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>
@@ -776,7 +776,7 @@
 
 subsection \<open>Package setup\<close>
 
-ML_file "Tools/hologic.ML"
+ML_file \<open>Tools/hologic.ML\<close>
 
 
 subsubsection \<open>Sledgehammer setup\<close>
@@ -1202,7 +1202,7 @@
 lemma ex_comm: "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   by blast
 
-ML_file "Tools/simpdata.ML"
+ML_file \<open>Tools/simpdata.ML\<close>
 ML \<open>open Simpdata\<close>
 
 setup \<open>
@@ -1484,7 +1484,7 @@
 
 text \<open>Method setup.\<close>
 
-ML_file "~~/src/Tools/induct.ML"
+ML_file \<open>~~/src/Tools/induct.ML\<close>
 ML \<open>
 structure Induct = Induct
 (
@@ -1499,7 +1499,7 @@
 )
 \<close>
 
-ML_file "~~/src/Tools/induction.ML"
+ML_file \<open>~~/src/Tools/induction.ML\<close>
 
 declaration \<open>
   fn _ => Induct.map_simpset (fn ss => ss
@@ -1584,12 +1584,12 @@
 
 end
 
-ML_file "~~/src/Tools/induct_tacs.ML"
+ML_file \<open>~~/src/Tools/induct_tacs.ML\<close>
 
 
 subsubsection \<open>Coherent logic\<close>
 
-ML_file "~~/src/Tools/coherent.ML"
+ML_file \<open>~~/src/Tools/coherent.ML\<close>
 ML \<open>
 structure Coherent = Coherent
 (
@@ -1735,7 +1735,7 @@
 val trans = @{thm trans}
 \<close>
 
-ML_file "Tools/cnf.ML"
+ML_file \<open>Tools/cnf.ML\<close>
 
 
 section \<open>\<open>NO_MATCH\<close> simproc\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/HOLCF/Cpodef.thy
--- a/src/HOL/HOLCF/Cpodef.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -279,6 +279,6 @@
 
 subsection \<open>HOLCF type definition package\<close>
 
-ML_file "Tools/cpodef.ML"
+ML_file \<open>Tools/cpodef.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -150,7 +150,7 @@
     (\<^const_name>\<open>liftprj\<close>, SOME \<^typ>\<open>udom u \<rightarrow> 'a::predomain u\<close>)]
 \<close>
 
-ML_file "Tools/domaindef.ML"
+ML_file \<open>Tools/domaindef.ML\<close>
 
 subsection \<open>Isomorphic deflations\<close>
 
@@ -319,9 +319,9 @@
 named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
   and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
 
-ML_file "Tools/Domain/domain_isomorphism.ML"
-ML_file "Tools/Domain/domain_axioms.ML"
-ML_file "Tools/Domain/domain.ML"
+ML_file \<open>Tools/Domain/domain_isomorphism.ML\<close>
+ML_file \<open>Tools/Domain/domain_axioms.ML\<close>
+ML_file \<open>Tools/Domain/domain.ML\<close>
 
 lemmas [domain_defl_simps] =
   DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/HOLCF/Domain_Aux.thy
--- a/src/HOL/HOLCF/Domain_Aux.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -355,10 +355,10 @@
 named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
   and domain_map_ID "theorems like foo_map$ID = ID"
 
-ML_file "Tools/Domain/domain_take_proofs.ML"
-ML_file "Tools/cont_consts.ML"
-ML_file "Tools/cont_proc.ML"
-ML_file "Tools/Domain/domain_constructors.ML"
-ML_file "Tools/Domain/domain_induction.ML"
+ML_file \<open>Tools/Domain/domain_take_proofs.ML\<close>
+ML_file \<open>Tools/cont_consts.ML\<close>
+ML_file \<open>Tools/cont_proc.ML\<close>
+ML_file \<open>Tools/Domain/domain_constructors.ML\<close>
+ML_file \<open>Tools/Domain/domain_induction.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -224,8 +224,8 @@
 
 subsection \<open>Initializing the fixrec package\<close>
 
-ML_file "Tools/holcf_library.ML"
-ML_file "Tools/fixrec.ML"
+ML_file \<open>Tools/holcf_library.ML\<close>
+ML_file \<open>Tools/fixrec.ML\<close>
 
 method_setup fixrec_simp = \<open>
   Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports IOA.IOA Env Impl Impl_finite
 begin
 
-ML_file "Check.ML"
+ML_file \<open>Check.ML\<close>
 
 primrec reduce :: "'a list => 'a list"
 where
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -903,7 +903,7 @@
 lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c"
   by (simp only: someI_ex)
 
-ML_file "Tools/choice_specification.ML"
+ML_file \<open>Tools/choice_specification.ML\<close>
 
 subsection \<open>Complete Distributive Lattices -- Properties depending on Hilbert Choice\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -53,7 +53,7 @@
  "_hoare"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
 
-ML_file "hoare_syntax.ML"
+ML_file \<open>hoare_syntax.ML\<close>
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close>
 
@@ -93,7 +93,7 @@
   by blast
 
 lemmas AbortRule = SkipRule  \<comment> \<open>dummy version\<close>
-ML_file "hoare_tac.ML"
+ML_file \<open>hoare_tac.ML\<close>
 
 method_setup vcg = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -55,7 +55,7 @@
   "_hoare_abort"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
 
-ML_file "hoare_syntax.ML"
+ML_file \<open>hoare_syntax.ML\<close>
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
 print_translation
   \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
@@ -104,7 +104,7 @@
 lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
   by blast
 
-ML_file "hoare_tac.ML"
+ML_file \<open>hoare_tac.ML\<close>
 
 method_setup vcg = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Import/Import_Setup.thy
--- a/src/HOL/Import/Import_Setup.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Import/Import_Setup.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
 keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
 begin
 
-ML_file "import_data.ML"
+ML_file \<open>import_data.ML\<close>
 
 lemma light_ex_imp_nonempty:
   "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
@@ -26,7 +26,7 @@
   "(\<And>x. f x = g x) \<Longrightarrow> f = g"
   by auto
 
-ML_file "import_rule.ML"
+ML_file \<open>import_rule.ML\<close>
 
 end
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Inductive.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -413,7 +413,7 @@
 lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
   by auto
 
-ML_file "Tools/inductive.ML"
+ML_file \<open>Tools/inductive.ML\<close>
 
 lemmas [mono] =
   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
@@ -514,14 +514,14 @@
 
 text \<open>Package setup.\<close>
 
-ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
-ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
-ML_file "Tools/Old_Datatype/old_datatype_data.ML"
-ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
-ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
-ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
-ML_file "Tools/Old_Datatype/old_primrec.ML"
-ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
+ML_file \<open>Tools/Old_Datatype/old_datatype_aux.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_datatype_prop.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_datatype_data.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_rep_datatype.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_datatype_codegen.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_util.ML\<close>
+ML_file \<open>Tools/Old_Datatype/old_primrec.ML\<close>
+ML_file \<open>Tools/BNF/bnf_lfp_rec_sugar.ML\<close>
 
 text \<open>Lambda-abstractions with pattern matching:\<close>
 syntax (ASCII)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Int.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -1081,7 +1081,7 @@
 lemmas of_int_simps =
   of_int_0 of_int_1 of_int_add of_int_mult
 
-ML_file "Tools/int_arith.ML"
+ML_file \<open>Tools/int_arith.ML\<close>
 declaration \<open>K Int_Arith.setup\<close>
 
 simproc_setup fast_arith
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -401,7 +401,7 @@
 
 lemmas AbortRule = SkipRule  \<comment> \<open>dummy version\<close>
 
-ML_file "~~/src/HOL/Hoare/hoare_tac.ML"
+ML_file \<open>~~/src/HOL/Hoare/hoare_tac.ML\<close>
 
 method_setup hoare =
   \<open>Scan.succeed (fn ctxt =>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Lattices.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -693,7 +693,7 @@
 
 end
 
-ML_file "Tools/boolean_algebra_cancel.ML"
+ML_file \<open>Tools/boolean_algebra_cancel.ML\<close>
 
 simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
   \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Adhoc_Overloading.thy
--- a/src/HOL/Library/Adhoc_Overloading.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Adhoc_Overloading.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -10,6 +10,6 @@
   keywords "adhoc_overloading" "no_adhoc_overloading" :: thy_decl
 begin
 
-ML_file "adhoc_overloading.ML"
+ML_file \<open>adhoc_overloading.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/BNF_Axiomatization.thy
--- a/src/HOL/Library/BNF_Axiomatization.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/BNF_Axiomatization.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -13,6 +13,6 @@
   "bnf_axiomatization" :: thy_decl
 begin
 
-ML_file "../Tools/BNF/bnf_axiomatization.ML"
+ML_file \<open>../Tools/BNF/bnf_axiomatization.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/BNF_Corec.thy
--- a/src/HOL/Library/BNF_Corec.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/BNF_Corec.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -201,12 +201,12 @@
 
 named_theorems friend_of_corec_simps
 
-ML_file "../Tools/BNF/bnf_gfp_grec_tactics.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec_sugar_util.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec_sugar.ML"
-ML_file "../Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_tactics.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar_util.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar_tactics.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_sugar.ML\<close>
+ML_file \<open>../Tools/BNF/bnf_gfp_grec_unique_sugar.ML\<close>
 
 method_setup transfer_prover_eq = \<open>
   Scan.succeed (SIMPLE_METHOD' o BNF_GFP_Grec_Tactics.transfer_prover_eq_tac)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Cancellation.thy
--- a/src/HOL/Library/Cancellation.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Cancellation.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -76,9 +76,9 @@
 
 subsection \<open>Simproc Set-Up\<close>
 
-ML_file "Cancellation/cancel.ML"
-ML_file "Cancellation/cancel_data.ML"
-ML_file "Cancellation/cancel_simprocs.ML"
+ML_file \<open>Cancellation/cancel.ML\<close>
+ML_file \<open>Cancellation/cancel_data.ML\<close>
+ML_file \<open>Cancellation/cancel_simprocs.ML\<close>
 
 end
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Case_Converter.thy
--- a/src/HOL/Library/Case_Converter.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Case_Converter.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -18,6 +18,6 @@
   "missing_pattern_match = Code.abort"
   unfolding missing_pattern_match_def Code.abort_def ..
 
-ML_file "case_converter.ML"
+ML_file \<open>case_converter.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Code_Lazy.thy
--- a/src/HOL/Library/Code_Lazy.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Code_Lazy.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -227,7 +227,7 @@
 
 subsection \<open>Implementation\<close>
 
-ML_file "code_lazy.ML"
+ML_file \<open>code_lazy.ML\<close>
 
 setup \<open>
   Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Code_Prolog.thy
--- a/src/HOL/Library/Code_Prolog.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Code_Prolog.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,7 +9,7 @@
 keywords "values_prolog" :: diag
 begin
 
-ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
+ML_file \<open>~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML\<close>
 
 section \<open>Setup for Numerals\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Code_Test.thy
--- a/src/HOL/Library/Code_Test.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Code_Test.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -142,6 +142,6 @@
 
 subsection \<open>Test engine and drivers\<close>
 
-ML_file "code_test.ML"
+ML_file \<open>code_test.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Conditional_Parametricity.thy
--- a/src/HOL/Library/Conditional_Parametricity.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Conditional_Parametricity.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -43,6 +43,6 @@
 
 end
 
-ML_file "conditional_parametricity.ML"
+ML_file \<open>conditional_parametricity.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Countable.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -200,7 +200,7 @@
 
 subsection \<open>Automatically proving countability of datatypes\<close>
 
-ML_file "../Tools/BNF/bnf_lfp_countable.ML"
+ML_file \<open>../Tools/BNF/bnf_lfp_countable.ML\<close>
 
 ML \<open>
 fun countable_datatype_tac ctxt st =
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Datatype_Records.thy
--- a/src/HOL/Library/Datatype_Records.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Datatype_Records.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -82,7 +82,7 @@
 
 named_theorems datatype_record_update
 
-ML_file "datatype_records.ML"
+ML_file \<open>datatype_records.ML\<close>
 setup \<open>Datatype_Records.setup\<close>
 
 end
\ No newline at end of file
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Multiset.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -969,7 +969,7 @@
   unfolding subset_mset_def repeat_mset_iterate_add
   by (simp add: iterate_add_eq_add_iff2 mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add])
 
-ML_file "multiset_simprocs.ML"
+ML_file \<open>multiset_simprocs.ML\<close>
 
 lemma add_mset_replicate_mset_safe[cancelation_simproc_pre]: \<open>NO_MATCH {#} M \<Longrightarrow> add_mset a M = {#a#} + M\<close>
   by simp
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -508,6 +508,6 @@
 hide_type (open) node item
 hide_const (open) Push Node Atom Leaf Numb Lim Split Case
 
-ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
+ML_file \<open>~~/src/HOL/Tools/Old_Datatype/old_datatype.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Old_Recdef.thy
--- a/src/HOL/Library/Old_Recdef.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Old_Recdef.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -57,7 +57,7 @@
 lemma tfl_exE: "\<exists>x. P x \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q \<Longrightarrow> Q"
   by blast
 
-ML_file "old_recdef.ML"
+ML_file \<open>old_recdef.ML\<close>
 
 
 subsection \<open>Rule setup\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Predicate_Compile_Quickcheck.thy
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,6 +8,6 @@
   imports Predicate_Compile_Alternative_Defs
 begin
 
-ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
+ML_file \<open>../Tools/Predicate_Compile/predicate_compile_quickcheck.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Realizers.thy
--- a/src/HOL/Library/Realizers.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Realizers.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
-ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
+ML_file \<open>~~/src/HOL/Tools/datatype_realizer.ML\<close>
+ML_file \<open>~~/src/HOL/Tools/inductive_realizer.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Reflection.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-ML_file "~~/src/HOL/Tools/reflection.ML"
+ML_file \<open>~~/src/HOL/Tools/reflection.ML\<close>
 
 method_setup reify = \<open>
   Attrib.thms --
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Refute.thy
--- a/src/HOL/Library/Refute.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Refute.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -14,7 +14,7 @@
   "refute_params" :: thy_decl
 begin
 
-ML_file "refute.ML"
+ML_file \<open>refute.ML\<close>
 
 refute_params
  [itself = 1,
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Rewrite.thy
--- a/src/HOL/Library/Rewrite.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Rewrite.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -30,7 +30,7 @@
    apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
   done
 
-ML_file "cconv.ML"
-ML_file "rewrite.ML"
+ML_file \<open>cconv.ML\<close>
+ML_file \<open>rewrite.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Simps_Case_Conv.thy
--- a/src/HOL/Library/Simps_Case_Conv.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Simps_Case_Conv.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,6 +8,6 @@
   abbrevs "simps_of_case" "case_of_simps" = ""
 begin
 
-ML_file "simps_case_conv.ML"
+ML_file \<open>simps_case_conv.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Library/Sum_of_Squares.thy
--- a/src/HOL/Library/Sum_of_Squares.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Library/Sum_of_Squares.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -10,9 +10,9 @@
 imports Complex_Main
 begin
 
-ML_file "positivstellensatz.ML"
-ML_file "Sum_of_Squares/sum_of_squares.ML"
-ML_file "Sum_of_Squares/positivstellensatz_tools.ML"
-ML_file "Sum_of_Squares/sos_wrapper.ML"
+ML_file \<open>positivstellensatz.ML\<close>
+ML_file \<open>Sum_of_Squares/sum_of_squares.ML\<close>
+ML_file \<open>Sum_of_Squares/positivstellensatz_tools.ML\<close>
+ML_file \<open>Sum_of_Squares/sos_wrapper.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Lifting.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -552,22 +552,22 @@
 
 subsection \<open>ML setup\<close>
 
-ML_file "Tools/Lifting/lifting_util.ML"
+ML_file \<open>Tools/Lifting/lifting_util.ML\<close>
 
 named_theorems relator_eq_onp
   "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
-ML_file "Tools/Lifting/lifting_info.ML"
+ML_file \<open>Tools/Lifting/lifting_info.ML\<close>
 
 (* setup for the function type *)
 declare fun_quotient[quot_map]
 declare fun_mono[relator_mono]
 lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
 
-ML_file "Tools/Lifting/lifting_bnf.ML"
-ML_file "Tools/Lifting/lifting_term.ML"
-ML_file "Tools/Lifting/lifting_def.ML"
-ML_file "Tools/Lifting/lifting_setup.ML"
-ML_file "Tools/Lifting/lifting_def_code_dt.ML"
+ML_file \<open>Tools/Lifting/lifting_bnf.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_term.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_def.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_setup.ML\<close>
+ML_file \<open>Tools/Lifting/lifting_def_code_dt.ML\<close>
 
 lemma pred_prod_beta: "pred_prod P Q xy \<longleftrightarrow> P (fst xy) \<and> Q (snd xy)"
 by(cases xy) simp
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports Complex_Main "HOL-Library.Lattice_Algebras"
 begin
 
-ML_file "~~/src/Tools/float.ML"
+ML_file \<open>~~/src/Tools/float.ML\<close>
 
 (*FIXME surely floor should be used? This file is full of redundant material.*)
 
@@ -235,6 +235,6 @@
 lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0
   nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false
 
-ML_file "float_arith.ML"
+ML_file \<open>float_arith.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
--- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -7,13 +7,13 @@
 theory Compute_Oracle imports HOL.HOL
 begin
 
-ML_file "am.ML"
-ML_file "am_compiler.ML"
-ML_file "am_interpreter.ML"
-ML_file "am_ghc.ML"
-ML_file "am_sml.ML"
-ML_file "report.ML"
-ML_file "compute.ML"
-ML_file "linker.ML"
+ML_file \<open>am.ML\<close>
+ML_file \<open>am_compiler.ML\<close>
+ML_file \<open>am_interpreter.ML\<close>
+ML_file \<open>am_ghc.ML\<close>
+ML_file \<open>am_sml.ML\<close>
+ML_file \<open>report.ML\<close>
+ML_file \<open>compute.ML\<close>
+ML_file \<open>linker.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Matrix_LP/Cplex.thy
--- a/src/HOL/Matrix_LP/Cplex.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Matrix_LP/Cplex.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -6,10 +6,10 @@
 imports SparseMatrix LP ComputeFloat ComputeNumeral
 begin
 
-ML_file "Cplex_tools.ML"
-ML_file "CplexMatrixConverter.ML"
-ML_file "FloatSparseMatrixBuilder.ML"
-ML_file "fspmlp.ML"
+ML_file \<open>Cplex_tools.ML\<close>
+ML_file \<open>CplexMatrixConverter.ML\<close>
+ML_file \<open>FloatSparseMatrixBuilder.ML\<close>
+ML_file \<open>fspmlp.ML\<close>
 
 lemma spm_mult_le_dual_prts: 
   assumes
@@ -64,7 +64,7 @@
   (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
   by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
 
-ML_file "matrixlp.ML"
+ML_file \<open>matrixlp.ML\<close>
 
 end
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Meson.thy
--- a/src/HOL/Meson.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Meson.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -195,9 +195,9 @@
 
 subsection \<open>Meson package\<close>
 
-ML_file "Tools/Meson/meson.ML"
-ML_file "Tools/Meson/meson_clausify.ML"
-ML_file "Tools/Meson/meson_tactic.ML"
+ML_file \<open>Tools/Meson/meson.ML\<close>
+ML_file \<open>Tools/Meson/meson_clausify.ML\<close>
+ML_file \<open>Tools/Meson/meson_tactic.ML\<close>
 
 hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem
 hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Metis.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
 imports ATP
 begin
 
-ML_file "~~/src/Tools/Metis/metis.ML"
+ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
 
 
 subsection \<open>Literal selection and lambda-lifting helpers\<close>
@@ -38,9 +38,9 @@
 
 subsection \<open>Metis package\<close>
 
-ML_file "Tools/Metis/metis_generate.ML"
-ML_file "Tools/Metis/metis_reconstruct.ML"
-ML_file "Tools/Metis/metis_tactic.ML"
+ML_file \<open>Tools/Metis/metis_generate.ML\<close>
+ML_file \<open>Tools/Metis/metis_reconstruct.ML\<close>
+ML_file \<open>Tools/Metis/metis_tactic.ML\<close>
 
 hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
 hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Mirabelle/Mirabelle.thy
--- a/src/HOL/Mirabelle/Mirabelle.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Mirabelle/Mirabelle.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -6,8 +6,8 @@
 imports Main
 begin
 
-ML_file "Tools/mirabelle.ML"
-ML_file "../TPTP/sledgehammer_tactics.ML"
+ML_file \<open>Tools/mirabelle.ML\<close>
+ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close>
 
 ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Mirabelle/Mirabelle_Test.thy
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,13 +8,13 @@
 imports Main Mirabelle
 begin
 
-ML_file "Tools/mirabelle_arith.ML"
-ML_file "Tools/mirabelle_metis.ML"
-ML_file "Tools/mirabelle_quickcheck.ML"
-ML_file "Tools/mirabelle_refute.ML"
-ML_file "Tools/mirabelle_sledgehammer.ML"
-ML_file "Tools/mirabelle_sledgehammer_filter.ML"
-ML_file "Tools/mirabelle_try0.ML"
+ML_file \<open>Tools/mirabelle_arith.ML\<close>
+ML_file \<open>Tools/mirabelle_metis.ML\<close>
+ML_file \<open>Tools/mirabelle_quickcheck.ML\<close>
+ML_file \<open>Tools/mirabelle_refute.ML\<close>
+ML_file \<open>Tools/mirabelle_sledgehammer.ML\<close>
+ML_file \<open>Tools/mirabelle_sledgehammer_filter.ML\<close>
+ML_file \<open>Tools/mirabelle_try0.ML\<close>
 
 text \<open>
   Only perform type-checking of the actions,
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Mutabelle/MutabelleExtra.thy
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -11,8 +11,8 @@
   "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
 begin
 
-ML_file "mutabelle.ML"
-ML_file "mutabelle_extra.ML"
+ML_file \<open>mutabelle.ML\<close>
+ML_file \<open>mutabelle_extra.ML\<close>
 
 
 section \<open>configuration\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nat.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -1930,7 +1930,7 @@
   shows "u = s"
   using assms(2,1) by (rule trans)
 
-ML_file "Tools/nat_arith.ML"
+ML_file \<open>Tools/nat_arith.ML\<close>
 
 simproc_setup nateq_cancel_sums
   ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nitpick.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -201,21 +201,21 @@
 definition wfrec' ::  "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   "wfrec' R F x \<equiv> if wf R then wf_wfrec' R F x else THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y"
 
-ML_file "Tools/Nitpick/kodkod.ML"
-ML_file "Tools/Nitpick/kodkod_sat.ML"
-ML_file "Tools/Nitpick/nitpick_util.ML"
-ML_file "Tools/Nitpick/nitpick_hol.ML"
-ML_file "Tools/Nitpick/nitpick_mono.ML"
-ML_file "Tools/Nitpick/nitpick_preproc.ML"
-ML_file "Tools/Nitpick/nitpick_scope.ML"
-ML_file "Tools/Nitpick/nitpick_peephole.ML"
-ML_file "Tools/Nitpick/nitpick_rep.ML"
-ML_file "Tools/Nitpick/nitpick_nut.ML"
-ML_file "Tools/Nitpick/nitpick_kodkod.ML"
-ML_file "Tools/Nitpick/nitpick_model.ML"
-ML_file "Tools/Nitpick/nitpick.ML"
-ML_file "Tools/Nitpick/nitpick_commands.ML"
-ML_file "Tools/Nitpick/nitpick_tests.ML"
+ML_file \<open>Tools/Nitpick/kodkod.ML\<close>
+ML_file \<open>Tools/Nitpick/kodkod_sat.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_util.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_hol.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_mono.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_preproc.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_scope.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_peephole.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_rep.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_nut.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_kodkod.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_model.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_commands.ML\<close>
+ML_file \<open>Tools/Nitpick/nitpick_tests.ML\<close>
 
 setup \<open>
   Nitpick_HOL.register_ersatz_global
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Nitpick_Examples/Mini_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-ML_file "minipick.ML"
+ML_file \<open>minipick.ML\<close>
 
 nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
   total_consts = smart]
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -3561,7 +3561,7 @@
 
 (*******************************************************)
 (* Setup of the theorem attributes eqvt and eqvt_force *)
-ML_file "nominal_thmdecls.ML"
+ML_file \<open>nominal_thmdecls.ML\<close>
 setup "NominalThmDecls.setup"
 
 lemmas [eqvt] = 
@@ -3597,11 +3597,11 @@
 (***************************************)
 (* setup for the individial atom-kinds *)
 (* and nominal datatypes               *)
-ML_file "nominal_atoms.ML"
+ML_file \<open>nominal_atoms.ML\<close>
 
 (************************************************************)
 (* various tactics for analysing permutations, supports etc *)
-ML_file "nominal_permeq.ML"
+ML_file \<open>nominal_permeq.ML\<close>
 
 method_setup perm_simp =
   \<open>NominalPermeq.perm_simp_meth\<close>
@@ -3645,7 +3645,7 @@
 
 (*****************************************************************)
 (* tactics for generating fresh names and simplifying fresh_funs *)
-ML_file "nominal_fresh_fun.ML"
+ML_file \<open>nominal_fresh_fun.ML\<close>
 
 method_setup generate_fresh = \<open>
   Args.type_name {proper = true, strict = true} >>
@@ -3663,20 +3663,20 @@
 lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
   using assms ..
 
-ML_file "nominal_datatype.ML"
+ML_file \<open>nominal_datatype.ML\<close>
 
 (******************************************************)
 (* primitive recursive functions on nominal datatypes *)
-ML_file "nominal_primrec.ML"
+ML_file \<open>nominal_primrec.ML\<close>
 
 (****************************************************)
 (* inductive definition involving nominal datatypes *)
-ML_file "nominal_inductive.ML"
-ML_file "nominal_inductive2.ML"
+ML_file \<open>nominal_inductive.ML\<close>
+ML_file \<open>nominal_inductive2.ML\<close>
 
 (*****************************************)
 (* setup for induction principles method *)
-ML_file "nominal_induct.ML"
+ML_file \<open>nominal_induct.ML\<close>
 method_setup nominal_induct =
   \<open>NominalInduct.nominal_induct_method\<close>
   \<open>nominal induction\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Nonstandard_Analysis/StarDef.thy
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -99,7 +99,7 @@
   where "star_of x \<equiv> star_n (\<lambda>n. x)"
 
 text \<open>Initialize transfer tactic.\<close>
-ML_file "transfer_principle.ML"
+ML_file \<open>transfer_principle.ML\<close>
 
 method_setup transfer =
   \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Num.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -292,7 +292,7 @@
 syntax
   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
 
-ML_file "Tools/numeral.ML"
+ML_file \<open>Tools/numeral.ML\<close>
 
 parse_translation \<open>
   let
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -6,11 +6,11 @@
 imports Divides
 begin
 
-ML_file "~~/src/Provers/Arith/assoc_fold.ML"
-ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
-ML_file "~~/src/Provers/Arith/combine_numerals.ML"
-ML_file "~~/src/Provers/Arith/cancel_numeral_factor.ML"
-ML_file "~~/src/Provers/Arith/extract_common_term.ML"
+ML_file \<open>~~/src/Provers/Arith/assoc_fold.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/cancel_numeral_factor.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/extract_common_term.ML\<close>
 
 lemmas semiring_norm =
   Let_def arith_simps diff_nat_numeral rel_simps
@@ -103,7 +103,7 @@
   fixes x:: "'a::comm_ring_1" shows  "numeral w * -x = x * - numeral w"
   by (simp add: mult.commute)
 
-ML_file "Tools/numeral_simprocs.ML"
+ML_file \<open>Tools/numeral_simprocs.ML\<close>
 
 simproc_setup semiring_assoc_fold
   ("(a::'a::comm_semiring_1_cancel) * b") =
@@ -213,7 +213,7 @@
   |"(l::'a::field) / (m * n)") =
   \<open>fn phi => Numeral_Simprocs.divide_cancel_factor\<close>
 
-ML_file "Tools/nat_numeral_simprocs.ML"
+ML_file \<open>Tools/nat_numeral_simprocs.ML\<close>
 
 simproc_setup nat_combine_numerals
   ("(i::nat) + j" | "Suc (i + j)") =
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Nunchaku.thy
--- a/src/HOL/Nunchaku.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Nunchaku.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -29,16 +29,16 @@
 definition rmember :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where
   "rmember A x \<longleftrightarrow> x \<in> A"
 
-ML_file "Tools/Nunchaku/nunchaku_util.ML"
-ML_file "Tools/Nunchaku/nunchaku_collect.ML"
-ML_file "Tools/Nunchaku/nunchaku_problem.ML"
-ML_file "Tools/Nunchaku/nunchaku_translate.ML"
-ML_file "Tools/Nunchaku/nunchaku_model.ML"
-ML_file "Tools/Nunchaku/nunchaku_reconstruct.ML"
-ML_file "Tools/Nunchaku/nunchaku_display.ML"
-ML_file "Tools/Nunchaku/nunchaku_tool.ML"
-ML_file "Tools/Nunchaku/nunchaku.ML"
-ML_file "Tools/Nunchaku/nunchaku_commands.ML"
+ML_file \<open>Tools/Nunchaku/nunchaku_util.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_collect.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_problem.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_translate.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_model.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_reconstruct.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_display.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_tool.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku.ML\<close>
+ML_file \<open>Tools/Nunchaku/nunchaku_commands.ML\<close>
 
 hide_const (open) unreachable The_unsafe rmember
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Orderings.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,8 +9,8 @@
 keywords "print_orders" :: diag
 begin
 
-ML_file "~~/src/Provers/order.ML"
-ML_file "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
+ML_file \<open>~~/src/Provers/order.ML\<close>
+ML_file \<open>~~/src/Provers/quasi.ML\<close>  (* FIXME unused? *)
 
 subsection \<open>Abstract ordering\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Partial_Function.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
 begin
 
 named_theorems partial_function_mono "monotonicity rules for partial function definitions"
-ML_file "Tools/Function/partial_function.ML"
+ML_file \<open>Tools/Function/partial_function.ML\<close>
 
 lemma (in ccpo) in_chain_finite:
   assumes "Complete_Partial_Order.chain (\<le>) A" "finite A" "A \<noteq> {}"
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Predicate_Compile.thy
--- a/src/HOL/Predicate_Compile.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Predicate_Compile.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -11,17 +11,17 @@
   "values" :: diag
 begin
 
-ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML"
-ML_file "Tools/Predicate_Compile/core_data.ML"
-ML_file "Tools/Predicate_Compile/mode_inference.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_proof.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_core.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_data.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
-ML_file "Tools/Predicate_Compile/predicate_compile.ML"
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_aux.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_compilations.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/core_data.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/mode_inference.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_proof.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_core.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_data.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_fun.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_pred.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile_specialisation.ML\<close>
+ML_file \<open>Tools/Predicate_Compile/predicate_compile.ML\<close>
 
 
 subsection \<open>Set membership as a generator predicate\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Presburger.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,8 +9,8 @@
 keywords "try0" :: diag
 begin
 
-ML_file "Tools/Qelim/qelim.ML"
-ML_file "Tools/Qelim/cooper_procedure.ML"
+ML_file \<open>Tools/Qelim/qelim.ML\<close>
+ML_file \<open>Tools/Qelim/cooper_procedure.ML\<close>
 
 subsection\<open>The \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Properties\<close>
 
@@ -390,7 +390,7 @@
   "\<lbrakk>x = x'; 0 \<le> x' \<Longrightarrow> P = P'\<rbrakk> \<Longrightarrow> (0 \<le> (x::int) \<and> P) = (0 \<le> x' \<and> P')"
   by (simp cong: conj_cong)
 
-ML_file "Tools/Qelim/cooper.ML"
+ML_file \<open>Tools/Qelim/cooper.ML\<close>
 
 method_setup presburger = \<open>
   let
@@ -505,6 +505,6 @@
 
 subsection \<open>Try0\<close>
 
-ML_file "Tools/try0.ML"
+ML_file \<open>Tools/try0.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Product_Type.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -738,7 +738,7 @@
 lemma internal_case_prod_conv: "internal_case_prod c (a, b) = c a b"
   by (simp only: internal_case_prod_def case_prod_conv)
 
-ML_file "Tools/split_rule.ML"
+ML_file \<open>Tools/split_rule.ML\<close>
 
 hide_const internal_case_prod
 
@@ -1263,7 +1263,7 @@
 
 subsection \<open>Simproc for rewriting a set comprehension into a pointfree expression\<close>
 
-ML_file "Tools/set_comprehension_pointfree.ML"
+ML_file \<open>Tools/set_comprehension_pointfree.ML\<close>
 
 setup \<open>
   Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
@@ -1309,7 +1309,7 @@
     | _ => NONE)
 \<close>
 
-ML_file "Tools/inductive_set.ML"
+ML_file \<open>Tools/inductive_set.ML\<close>
 
 
 subsection \<open>Legacy theorem bindings and duplicates\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Prolog/HOHH.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports HOL.HOL
 begin
 
-ML_file "prolog.ML"
+ML_file \<open>prolog.ML\<close>
 
 method_setup ptac =
   \<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -206,7 +206,7 @@
   @{thm [display] pigeonhole_slow_def}
   The program for searching for an element in an array is
   @{thm [display,eta_contract=false] search_def}
-  The correctness statement for @{term "pigeonhole"} is
+  The correctness statement for \<^term>\<open>pigeonhole\<close> is
   @{thm [display] pigeonhole_correctness [no_vars]}
 
   In order to analyze the speed of the above programs,
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -705,14 +705,14 @@
 
 notation (output) unknown  ("?")
 
-ML_file "Tools/Quickcheck/exhaustive_generators.ML"
+ML_file \<open>Tools/Quickcheck/exhaustive_generators.ML\<close>
 
 declare [[quickcheck_batch_tester = exhaustive]]
 
 
 subsection \<open>Defining generators for abstract types\<close>
 
-ML_file "Tools/Quickcheck/abstract_generators.ML"
+ML_file \<open>Tools/Quickcheck/abstract_generators.ML\<close>
 
 hide_fact (open) orelse_def
 no_notation orelse  (infixr "orelse" 55)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -192,9 +192,9 @@
 
 subsubsection \<open>Setting up the counterexample generator\<close>
 
-external_file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
-external_file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
-ML_file "Tools/Quickcheck/narrowing_generators.ML"
+external_file \<open>~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs\<close>
+external_file \<open>~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs\<close>
+ML_file \<open>Tools/Quickcheck/narrowing_generators.ML\<close>
 
 definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
 where
@@ -318,7 +318,7 @@
 
 subsection \<open>The \<open>find_unused_assms\<close> command\<close>
 
-ML_file "Tools/Quickcheck/find_unused_assms.ML"
+ML_file \<open>Tools/Quickcheck/find_unused_assms.ML\<close>
 
 subsection \<open>Closing up\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Quickcheck_Random.thy
--- a/src/HOL/Quickcheck_Random.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Quickcheck_Random.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -209,8 +209,8 @@
 
 subsection \<open>Deriving random generators for datatypes\<close>
 
-ML_file "Tools/Quickcheck/quickcheck_common.ML"
-ML_file "Tools/Quickcheck/random_generators.ML"
+ML_file \<open>Tools/Quickcheck/quickcheck_common.ML\<close>
+ML_file \<open>Tools/Quickcheck/random_generators.ML\<close>
 
 
 subsection \<open>Code setup\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Quotient.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -636,7 +636,7 @@
   and quot_preserve "preservation theorems"
   and id_simps "identity simp rules for maps"
   and quot_thm "quotient theorems"
-ML_file "Tools/Quotient/quotient_info.ML"
+ML_file \<open>Tools/Quotient/quotient_info.ML\<close>
 
 declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
 
@@ -657,15 +657,15 @@
   vimage_id
 
 text \<open>Translation functions for the lifting process.\<close>
-ML_file "Tools/Quotient/quotient_term.ML"
+ML_file \<open>Tools/Quotient/quotient_term.ML\<close>
 
 
 text \<open>Definitions of the quotient types.\<close>
-ML_file "Tools/Quotient/quotient_type.ML"
+ML_file \<open>Tools/Quotient/quotient_type.ML\<close>
 
 
 text \<open>Definitions for quotient constants.\<close>
-ML_file "Tools/Quotient/quotient_def.ML"
+ML_file \<open>Tools/Quotient/quotient_def.ML\<close>
 
 
 text \<open>
@@ -692,7 +692,7 @@
 begin
 
 text \<open>Tactics for proving the lifted theorems\<close>
-ML_file "Tools/Quotient/quotient_tacs.ML"
+ML_file \<open>Tools/Quotient/quotient_tacs.ML\<close>
 
 end
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Real.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -1644,8 +1644,8 @@
 
 subsection \<open>Setup for SMT\<close>
 
-ML_file "Tools/SMT/smt_real.ML"
-ML_file "Tools/SMT/z3_real.ML"
+ML_file \<open>Tools/SMT/smt_real.ML\<close>
+ML_file \<open>Tools/SMT/z3_real.ML\<close>
 
 lemma [z3_rule]:
   "0 + x = x"
@@ -1660,6 +1660,6 @@
 
 subsection \<open>Setup for Argo\<close>
 
-ML_file "Tools/Argo/argo_real.ML"
+ML_file \<open>Tools/Argo/argo_real.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy
--- a/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -3,7 +3,7 @@
   imports "HOL-Real_Asymp.Real_Asymp"
 begin
 
-ML_file "~~/src/Doc/antiquote_setup.ML"
+ML_file \<open>~~/src/Doc/antiquote_setup.ML\<close>
 (*>*)
 
 section \<open>Introduction\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Record.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -453,7 +453,7 @@
 
 subsection \<open>Record package\<close>
 
-ML_file "Tools/record.ML"
+ML_file \<open>Tools/record.ML\<close>
 
 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Rings.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -1762,9 +1762,9 @@
 text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
 
 named_theorems arith "arith facts -- only ground formulas"
-ML_file "Tools/arith_data.ML"
-
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+ML_file \<open>Tools/arith_data.ML\<close>
+
+ML_file \<open>~~/src/Provers/Arith/cancel_div_mod.ML\<close>
 
 ML \<open>
 structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SAT.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -11,10 +11,10 @@
 imports Argo
 begin
 
-ML_file "Tools/prop_logic.ML"
-ML_file "Tools/sat_solver.ML"
-ML_file "Tools/sat.ML"
-ML_file "Tools/Argo/argo_sat_solver.ML"
+ML_file \<open>Tools/prop_logic.ML\<close>
+ML_file \<open>Tools/sat_solver.ML\<close>
+ML_file \<open>Tools/sat.ML\<close>
+ML_file \<open>Tools/Argo/argo_sat_solver.ML\<close>
 
 method_setup sat = \<open>Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac)\<close>
   "SAT solver"
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SMT.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -286,35 +286,35 @@
 
 subsection \<open>Setup\<close>
 
-ML_file "Tools/SMT/smt_util.ML"
-ML_file "Tools/SMT/smt_failure.ML"
-ML_file "Tools/SMT/smt_config.ML"
-ML_file "Tools/SMT/smt_builtin.ML"
-ML_file "Tools/SMT/smt_datatypes.ML"
-ML_file "Tools/SMT/smt_normalize.ML"
-ML_file "Tools/SMT/smt_translate.ML"
-ML_file "Tools/SMT/smtlib.ML"
-ML_file "Tools/SMT/smtlib_interface.ML"
-ML_file "Tools/SMT/smtlib_proof.ML"
-ML_file "Tools/SMT/smtlib_isar.ML"
-ML_file "Tools/SMT/z3_proof.ML"
-ML_file "Tools/SMT/z3_isar.ML"
-ML_file "Tools/SMT/smt_solver.ML"
-ML_file "Tools/SMT/cvc4_interface.ML"
-ML_file "Tools/SMT/cvc4_proof_parse.ML"
-ML_file "Tools/SMT/verit_proof.ML"
-ML_file "Tools/SMT/verit_isar.ML"
-ML_file "Tools/SMT/verit_proof_parse.ML"
-ML_file "Tools/SMT/conj_disj_perm.ML"
-ML_file "Tools/SMT/smt_replay_methods.ML"
-ML_file "Tools/SMT/smt_replay.ML"
-ML_file "Tools/SMT/z3_interface.ML"
-ML_file "Tools/SMT/z3_replay_rules.ML"
-ML_file "Tools/SMT/z3_replay_methods.ML"
-ML_file "Tools/SMT/z3_replay.ML"
-ML_file "Tools/SMT/verit_replay_methods.ML"
-ML_file "Tools/SMT/verit_replay.ML"
-ML_file "Tools/SMT/smt_systems.ML"
+ML_file \<open>Tools/SMT/smt_util.ML\<close>
+ML_file \<open>Tools/SMT/smt_failure.ML\<close>
+ML_file \<open>Tools/SMT/smt_config.ML\<close>
+ML_file \<open>Tools/SMT/smt_builtin.ML\<close>
+ML_file \<open>Tools/SMT/smt_datatypes.ML\<close>
+ML_file \<open>Tools/SMT/smt_normalize.ML\<close>
+ML_file \<open>Tools/SMT/smt_translate.ML\<close>
+ML_file \<open>Tools/SMT/smtlib.ML\<close>
+ML_file \<open>Tools/SMT/smtlib_interface.ML\<close>
+ML_file \<open>Tools/SMT/smtlib_proof.ML\<close>
+ML_file \<open>Tools/SMT/smtlib_isar.ML\<close>
+ML_file \<open>Tools/SMT/z3_proof.ML\<close>
+ML_file \<open>Tools/SMT/z3_isar.ML\<close>
+ML_file \<open>Tools/SMT/smt_solver.ML\<close>
+ML_file \<open>Tools/SMT/cvc4_interface.ML\<close>
+ML_file \<open>Tools/SMT/cvc4_proof_parse.ML\<close>
+ML_file \<open>Tools/SMT/verit_proof.ML\<close>
+ML_file \<open>Tools/SMT/verit_isar.ML\<close>
+ML_file \<open>Tools/SMT/verit_proof_parse.ML\<close>
+ML_file \<open>Tools/SMT/conj_disj_perm.ML\<close>
+ML_file \<open>Tools/SMT/smt_replay_methods.ML\<close>
+ML_file \<open>Tools/SMT/smt_replay.ML\<close>
+ML_file \<open>Tools/SMT/z3_interface.ML\<close>
+ML_file \<open>Tools/SMT/z3_replay_rules.ML\<close>
+ML_file \<open>Tools/SMT/z3_replay_methods.ML\<close>
+ML_file \<open>Tools/SMT/z3_replay.ML\<close>
+ML_file \<open>Tools/SMT/verit_replay_methods.ML\<close>
+ML_file \<open>Tools/SMT/verit_replay.ML\<close>
+ML_file \<open>Tools/SMT/smt_systems.ML\<close>
 
 method_setup smt = \<open>
   Scan.optional Attrib.thms [] >>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SMT_Examples/Boogie.thy
--- a/src/HOL/SMT_Examples/Boogie.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SMT_Examples/Boogie.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -45,7 +45,7 @@
 
 section \<open>Setup\<close>
 
-ML_file "boogie.ML"
+ML_file \<open>boogie.ML\<close>
 
 
 
@@ -55,22 +55,22 @@
 declare [[smt_read_only_certificates = true]]
 
 
-external_file "Boogie_Max.certs"
+external_file \<open>Boogie_Max.certs\<close>
 declare [[smt_certificates = "Boogie_Max.certs"]]
 
-boogie_file Boogie_Max
+boogie_file \<open>Boogie_Max\<close>
 
 
-external_file "Boogie_Dijkstra.certs"
+external_file \<open>Boogie_Dijkstra.certs\<close>
 declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
 
-boogie_file Boogie_Dijkstra
+boogie_file \<open>Boogie_Dijkstra\<close>
 
 
 declare [[z3_extensions = true]]
-external_file "VCC_Max.certs"
+external_file \<open>VCC_Max.certs\<close>
 declare [[smt_certificates = "VCC_Max.certs"]]
 
-boogie_file VCC_Max
+boogie_file \<open>VCC_Max\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-external_file "SMT_Examples.certs"
+external_file \<open>SMT_Examples.certs\<close>
 declare [[smt_certificates = "SMT_Examples.certs"]]
 declare [[smt_read_only_certificates = true]]
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
 spark_proof_functions
   gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
 
-spark_open "greatest_common_divisor/g_c_d"
+spark_open \<open>greatest_common_divisor/g_c_d\<close>
 
 spark_vc procedure_g_c_d_4
 proof -
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -541,7 +541,7 @@
 
 text \<open>The verification conditions\<close>
 
-spark_open "liseq/liseq_length"
+spark_open \<open>liseq/liseq_length\<close>
 
 spark_vc procedure_liseq_length_5
   by (simp_all add: liseq_singleton liseq'_singleton)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/RIPEMD-160/F.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/F.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports RMD_Specification
 begin
 
-spark_open "rmd/f"
+spark_open \<open>rmd/f\<close>
 
 spark_vc function_f_2
   using assms by simp_all
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports RMD_Specification
 begin
 
-spark_open "rmd/hash"
+spark_open \<open>rmd/hash\<close>
 
 abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where
   "from_chain c \<equiv> (
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports RMD_Specification
 begin
 
-spark_open "rmd/k_l"
+spark_open \<open>rmd/k_l\<close>
 
 spark_vc function_k_l_6
   using assms by (simp add: K_def)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports RMD_Specification
 begin
 
-spark_open "rmd/k_r"
+spark_open \<open>rmd/k_r\<close>
 
 spark_vc function_k_r_6
   using assms by (simp add: K'_def)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports RMD_Specification RMD_Lemmas
 begin
 
-spark_open "rmd/r_l"
+spark_open \<open>rmd/r_l\<close>
 
 spark_vc function_r_l_2
 proof -
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports RMD_Specification RMD_Lemmas
 begin
 
-spark_open "rmd/r_r"
+spark_open \<open>rmd/r_r\<close>
 
 spark_vc function_r_r_2
 proof -
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports RMD_Specification
 begin
 
-spark_open "rmd/round"
+spark_open \<open>rmd/round\<close>
 
 abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where
   "from_chain c \<equiv> (
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports RMD_Specification RMD_Lemmas
 begin
 
-spark_open "rmd/s_l"
+spark_open \<open>rmd/s_l\<close>
 
 spark_vc function_s_l_2
 proof -
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports RMD_Specification RMD_Lemmas
 begin
 
-spark_open "rmd/s_r"
+spark_open \<open>rmd/s_r\<close>
 
 spark_vc function_s_r_2
 proof -
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Examples/Sqrt/Sqrt.thy
--- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -7,7 +7,7 @@
 imports "HOL-SPARK.SPARK"
 begin
 
-spark_open "sqrt/isqrt"
+spark_open \<open>sqrt/isqrt\<close>
 
 spark_vc function_isqrt_4
 proof -
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Manual/Complex_Types.thy
--- a/src/HOL/SPARK/Manual/Complex_Types.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Manual/Complex_Types.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -31,7 +31,7 @@
   complex_types__initialized3 = initialized3
 
 (*<*)
-spark_open "complex_types_app/initialize"
+spark_open \<open>complex_types_app/initialize\<close>
 
 spark_vc procedure_initialize_1
   by (simp add: initialized_def)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Manual/Proc1.thy
--- a/src/HOL/SPARK/Manual/Proc1.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Manual/Proc1.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -2,7 +2,7 @@
 imports "HOL-SPARK.SPARK"
 begin
 
-spark_open "loop_invariant/proc1"
+spark_open \<open>loop_invariant/proc1\<close>
 
 spark_vc procedure_proc1_5
   by (simp add: ring_distribs mod_simps)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Manual/Proc2.thy
--- a/src/HOL/SPARK/Manual/Proc2.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Manual/Proc2.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -2,7 +2,7 @@
 imports "HOL-SPARK.SPARK"
 begin
 
-spark_open "loop_invariant/proc2"
+spark_open \<open>loop_invariant/proc2\<close>
 
 spark_vc procedure_proc2_7
   by (simp add: ring_distribs mod_simps)
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
--- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
 spark_proof_functions
   gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
 
-spark_open "simple_greatest_common_divisor/g_c_d"
+spark_open \<open>simple_greatest_common_divisor/g_c_d\<close>
 
 spark_vc procedure_g_c_d_4
   using \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -15,8 +15,8 @@
   "spark_status" :: diag
 begin
 
-ML_file "Tools/fdl_lexer.ML"
-ML_file "Tools/fdl_parser.ML"
+ML_file \<open>Tools/fdl_lexer.ML\<close>
+ML_file \<open>Tools/fdl_parser.ML\<close>
 
 text \<open>
 SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual
@@ -181,7 +181,7 @@
 
 text \<open>Load the package\<close>
 
-ML_file "Tools/spark_vcs.ML"
-ML_file "Tools/spark_commands.ML"
+ML_file \<open>Tools/spark_vcs.ML\<close>
+ML_file \<open>Tools/spark_commands.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -67,7 +67,7 @@
 
 text \<open>Semiring normalization proper\<close>
 
-ML_file "Tools/semiring_normalizer.ML"
+ML_file \<open>Tools/semiring_normalizer.ML\<close>
 
 context comm_semiring_1
 begin
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Sledgehammer.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -16,23 +16,23 @@
 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
   by (erule contrapos_nn) (rule arg_cong)
 
-ML_file "Tools/Sledgehammer/async_manager_legacy.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
-ML_file "Tools/Sledgehammer/sledgehammer.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
+ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_compress.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_minimize.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_isar.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -630,6 +630,6 @@
 text \<open>Now we have all the theorems in place that are needed for the
 certificate generating ML functions.\<close>
 
-ML_file "distinct_tree_prover.ML"
+ML_file \<open>distinct_tree_prover.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Statespace/StateSpaceLocale.thy
--- a/src/HOL/Statespace/StateSpaceLocale.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,8 +8,8 @@
 keywords "statespace" :: thy_decl
 begin
 
-ML_file "state_space.ML"
-ML_file "state_fun.ML"
+ML_file \<open>state_space.ML\<close>
+ML_file \<open>state_fun.ML\<close>
 
 text \<open>For every type that is to be stored in a state space, an
 instance of this locale is imported in order convert the abstract and
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/String.thy
--- a/src/HOL/String.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/String.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -200,7 +200,7 @@
 syntax
   "_String" :: "str_position \<Rightarrow> string"    ("_")
 
-ML_file "Tools/string_syntax.ML"
+ML_file \<open>Tools/string_syntax.ML\<close>
 
 instantiation char :: enum
 begin
@@ -458,7 +458,7 @@
   "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
   "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
 
-ML_file "Tools/literal.ML"
+ML_file \<open>Tools/literal.ML\<close>
 
 
 subsubsection \<open>Operations\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/TPTP/ATP_Problem_Import.thy
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports Complex_Main TPTP_Interpret "HOL-Library.Refute"
 begin
 
-ML_file "sledgehammer_tactics.ML"
+ML_file \<open>sledgehammer_tactics.ML\<close>
 
 ML \<open>Proofterm.proofs := 0\<close>
 
@@ -18,7 +18,7 @@
 declare [[unify_search_bound = 60]]
 declare [[unify_trace_bound = 60]]
 
-ML_file "atp_problem_import.ML"
+ML_file \<open>atp_problem_import.ML\<close>
 
 (*
 ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/TPTP/ATP_Theory_Export.thy
--- a/src/HOL/TPTP/ATP_Theory_Export.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-ML_file "atp_theory_export.ML"
+ML_file \<open>atp_theory_export.ML\<close>
 
 ML \<open>
 open ATP_Problem
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports MaSh_Export_Base
 begin
 
-ML_file "mash_eval.ML"
+ML_file \<open>mash_eval.ML\<close>
 
 sledgehammer_params
   [provers = e, max_facts = 64, strict, dont_slice, type_enc = poly_guards??,
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/TPTP/MaSh_Export_Base.thy
--- a/src/HOL/TPTP/MaSh_Export_Base.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-ML_file "mash_export.ML"
+ML_file \<open>mash_export.ML\<close>
 
 sledgehammer_params
   [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/TPTP/TPTP_Interpret.thy
--- a/src/HOL/TPTP/TPTP_Interpret.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -12,6 +12,6 @@
 
 typedecl ind
 
-ML_file "TPTP_Parser/tptp_interpret.ML"
+ML_file \<open>TPTP_Parser/tptp_interpret.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/TPTP/TPTP_Parser.thy
--- a/src/HOL/TPTP/TPTP_Parser.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/TPTP_Parser.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,13 +8,13 @@
 imports Pure
 begin
 
-ML_file "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
+ML_file \<open>TPTP_Parser/ml_yacc_lib.ML\<close> (*generated from ML-Yacc's lib*)
 
-ML_file "TPTP_Parser/tptp_syntax.ML"
-ML_file "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
-ML_file "TPTP_Parser/tptp_parser.ML"
-ML_file "TPTP_Parser/tptp_problem_name.ML"
-ML_file "TPTP_Parser/tptp_proof.ML"
+ML_file \<open>TPTP_Parser/tptp_syntax.ML\<close>
+ML_file \<open>TPTP_Parser/tptp_lexyacc.ML\<close> (*generated from tptp.lex and tptp.yacc*)
+ML_file \<open>TPTP_Parser/tptp_parser.ML\<close>
+ML_file \<open>TPTP_Parser/tptp_problem_name.ML\<close>
+ML_file \<open>TPTP_Parser/tptp_proof.ML\<close>
 
 text \<open>The TPTP parser was generated using ML-Yacc, and needs the
 ML-Yacc library to operate.  This library is included with the parser,
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -75,9 +75,9 @@
   tptp_informative_failure = true
 ]]
 
-ML_file "TPTP_Parser/tptp_reconstruct_library.ML"
+ML_file \<open>TPTP_Parser/tptp_reconstruct_library.ML\<close>
 ML "open TPTP_Reconstruct_Library"
-ML_file "TPTP_Parser/tptp_reconstruct.ML"
+ML_file \<open>TPTP_Parser/tptp_reconstruct.ML\<close>
 
 (*FIXME fudge*)
 declare [[
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Transfer.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -230,7 +230,7 @@
 
 
 
-ML_file "Tools/Transfer/transfer.ML"
+ML_file \<open>Tools/Transfer/transfer.ML\<close>
 declare refl [transfer_rule]
 
 hide_const (open) Rel
@@ -362,8 +362,8 @@
   "(if \<not> P then t else e) = (if P then e else t)"
 by auto
 
-ML_file "Tools/Transfer/transfer_bnf.ML"
-ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
+ML_file \<open>Tools/Transfer/transfer_bnf.ML\<close>
+ML_file \<open>Tools/BNF/bnf_fp_rec_sugar_transfer.ML\<close>
 
 declare pred_fun_def [simp]
 declare rel_fun_eq [relator_eq]
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -12,7 +12,7 @@
     and "^=" = "\<^sup>=" "\<^sup>=\<^sup>="
 begin
 
-ML_file "~~/src/Provers/trancl.ML"
+ML_file \<open>~~/src/Provers/trancl.ML\<close>
 
 text \<open>
   \<open>rtrancl\<close> is reflexive/transitive closure,
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Typedef.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -108,6 +108,6 @@
 
 end
 
-ML_file "Tools/typedef.ML"
+ML_file \<open>Tools/typedef.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Types_To_Sets/Types_To_Sets.thy
--- a/src/HOL/Types_To_Sets/Types_To_Sets.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -16,13 +16,13 @@
 subsection \<open>Rules\<close>
 
 text\<open>The following file implements the Local Typedef Rule (LT) and extends the logic by the rule.\<close>
-ML_file "local_typedef.ML"
+ML_file \<open>local_typedef.ML\<close>
 
 text\<open>The following file implements the Unoverloading Rule (UO) and extends the logic by the rule.\<close>
-ML_file "unoverloading.ML"
+ML_file \<open>unoverloading.ML\<close>
 
 text\<open>The following file implements a derived rule that internalizes type class annotations.\<close>
-ML_file "internalize_sort.ML"
+ML_file \<open>internalize_sort.ML\<close>
 
 text\<open>The following file provides some automation to unoverload and internalize the parameters o
   the sort constraints of a type variable.\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,7 +9,7 @@
 imports Detects PPROD Follows ProgressSets
 begin
 
-ML_file "UNITY_tactics.ML"
+ML_file \<open>UNITY_tactics.ML\<close>
 
 method_setup safety = \<open>
     Scan.succeed (SIMPLE_METHOD' o constrains_tac)\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/Word/Word.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -4502,8 +4502,8 @@
 
 declare bin_to_bl_def [simp]
 
-ML_file "Tools/word_lib.ML"
-ML_file "Tools/smt_word.ML"
+ML_file \<open>Tools/word_lib.ML\<close>
+ML_file \<open>Tools/smt_word.ML\<close>
 
 hide_const (open) Word
 
diff -r 86e8e7347ac0 -r 157990515be1 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -123,11 +123,11 @@
 text \<open>
   \<^ML>\<open>
       (
-        @{term \<open>""\<close>};
-        @{term \<open>"abc"\<close>};
-        @{term \<open>"abc" @ "xyz"\<close>};
-        @{term \<open>"\<newline>"\<close>};
-        @{term \<open>"\001\010\100"\<close>}
+        \<^term>\<open>""\<close>;
+        \<^term>\<open>"abc"\<close>;
+        \<^term>\<open>"abc" @ "xyz"\<close>;
+        \<^term>\<open>"\<newline>"\<close>;
+        \<^term>\<open>"\001\010\100"\<close>
       )
     \<close>
 \<close>
@@ -146,11 +146,11 @@
 \<open>
   \<^ML>\<open>
       (
-        @{term \<open>""\<close>};
-        @{term \<open>"abc"\<close>};
-        @{term \<open>"abc" @ "xyz"\<close>};
-        @{term \<open>"\<newline>"\<close>};
-        @{term \<open>"\001\010\100"\<close>}
+        \<^term>\<open>""\<close>;
+        \<^term>\<open>"abc"\<close>;
+        \<^term>\<open>"abc" @ "xyz"\<close>;
+        \<^term>\<open>"\<newline>"\<close>;
+        \<^term>\<open>"\001\010\100"\<close>
       )
     \<close>
 \<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Pure/Isar/token.scala	Sun Jan 06 15:11:13 2019 +0100
@@ -156,6 +156,15 @@
   val newline: Token = explode(Keyword.Keywords.empty, "\n").head
 
 
+  /* embedded */
+
+  def read_embedded(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] =
+    explode(keywords, inp) match {
+      case List(tok) if tok.is_embedded => Some(tok)
+      case _ => None
+    }
+
+
   /* names */
 
   def read_name(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] =
diff -r 86e8e7347ac0 -r 157990515be1 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Pure/Tools/update.scala	Sun Jan 06 15:11:13 2019 +0100
@@ -31,10 +31,18 @@
         session_dirs = dirs ::: select_dirs,
         include_sessions = deps.sessions_structure.imports_topological_order)
 
+    val path_cartouches = dump_options.bool("update_path_cartouches")
+
     def update_xml(xml: XML.Body): XML.Body =
       xml flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
           if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)
+        case XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), body)
+        if path_cartouches =>
+          Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
+            case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
+            case None => update_xml(body)
+          }
         case XML.Elem(_, body) => update_xml(body)
         case t => List(t)
       }
@@ -48,7 +56,7 @@
           for ((node_name, node) <- snapshot.nodes) {
             val xml =
               snapshot.state.markup_to_XML(snapshot.version, node_name,
-                Text.Range.full, Markup.Elements(Markup.UPDATE))
+                Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
 
             val source1 = Symbol.encode(XML.content(update_xml(xml)))
             if (source1 != Symbol.encode(node.source)) {
diff -r 86e8e7347ac0 -r 157990515be1 src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Sequents/LK.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -200,7 +200,7 @@
 lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x"
   by (fast add!: subst)
 
-ML_file "simpdata.ML"
+ML_file \<open>simpdata.ML\<close>
 setup \<open>map_theory_simpset (put_simpset LK_ss)\<close>
 setup \<open>Simplifier.method_setup []\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Sequents/Modal0.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -7,7 +7,7 @@
 imports LK0
 begin
 
-ML_file "modal.ML"
+ML_file \<open>modal.ML\<close>
 
 consts
   box           :: "o\<Rightarrow>o"       ("[]_" [50] 50)
diff -r 86e8e7347ac0 -r 157990515be1 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Sequents/Sequents.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -144,6 +144,6 @@
 
 subsection \<open>Proof tools\<close>
 
-ML_file "prover.ML"
+ML_file \<open>prover.ML\<close>
 
 end
diff -r 86e8e7347ac0 -r 157990515be1 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Tools/Code_Generator.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -16,17 +16,17 @@
     :: quasi_command
 begin
 
-ML_file "~~/src/Tools/cache_io.ML"
-ML_file "~~/src/Tools/Code/code_preproc.ML"
-ML_file "~~/src/Tools/Code/code_symbol.ML"
-ML_file "~~/src/Tools/Code/code_thingol.ML"
-ML_file "~~/src/Tools/Code/code_simp.ML"
-ML_file "~~/src/Tools/Code/code_printer.ML"
-ML_file "~~/src/Tools/Code/code_target.ML"
-ML_file "~~/src/Tools/Code/code_namespace.ML"
-ML_file "~~/src/Tools/Code/code_ml.ML"
-ML_file "~~/src/Tools/Code/code_haskell.ML"
-ML_file "~~/src/Tools/Code/code_scala.ML"
+ML_file \<open>~~/src/Tools/cache_io.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_preproc.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_symbol.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_thingol.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_simp.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_printer.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_target.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_namespace.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_ml.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_haskell.ML\<close>
+ML_file \<open>~~/src/Tools/Code/code_scala.ML\<close>
 
 code_datatype "TYPE('a::{})"
 
@@ -55,8 +55,8 @@
     by rule (rule holds)+
 qed  
 
-ML_file "~~/src/Tools/Code/code_runtime.ML"
-ML_file "~~/src/Tools/nbe.ML"
+ML_file \<open>~~/src/Tools/Code/code_runtime.ML\<close>
+ML_file \<open>~~/src/Tools/nbe.ML\<close>
 
 hide_const (open) holds
 
diff -r 86e8e7347ac0 -r 157990515be1 src/Tools/SML/Examples.thy
--- a/src/Tools/SML/Examples.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Tools/SML/Examples.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -21,7 +21,7 @@
   evaluates it for some arguments.
 \<close>
 
-SML_file "factorial.sml"
+SML_file \<open>factorial.sml\<close>
 
 text \<open>
   The subsequent example illustrates the use of multiple \<^theory_text>\<open>SML_file\<close> commands
@@ -30,8 +30,8 @@
   independently of the Isabelle/ML environment.
 \<close>
 
-SML_file "Example.sig"
-SML_file "Example.sml"
+SML_file \<open>Example.sig\<close>
+SML_file \<open>Example.sml\<close>
 
 
 text \<open>
diff -r 86e8e7347ac0 -r 157990515be1 src/Tools/Spec_Check/Spec_Check.thy
--- a/src/Tools/Spec_Check/Spec_Check.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/Tools/Spec_Check/Spec_Check.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -2,12 +2,12 @@
 imports Pure
 begin
 
-ML_file "random.ML"
-ML_file "property.ML"
-ML_file "base_generator.ML"
-ML_file "generator.ML"
-ML_file "gen_construction.ML"
-ML_file "spec_check.ML"
-ML_file "output_style.ML"
+ML_file \<open>random.ML\<close>
+ML_file \<open>property.ML\<close>
+ML_file \<open>base_generator.ML\<close>
+ML_file \<open>generator.ML\<close>
+ML_file \<open>gen_construction.ML\<close>
+ML_file \<open>spec_check.ML\<close>
+ML_file \<open>output_style.ML\<close>
 
 end
\ No newline at end of file
diff -r 86e8e7347ac0 -r 157990515be1 src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/ArithSimp.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -9,9 +9,9 @@
 imports Arith
 begin
 
-ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
-ML_file "~~/src/Provers/Arith/combine_numerals.ML"
-ML_file "arith_data.ML"
+ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
+ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
+ML_file \<open>arith_data.ML\<close>
 
 
 subsection\<open>Difference\<close>
diff -r 86e8e7347ac0 -r 157990515be1 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/Bin.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -117,7 +117,7 @@
   "_Int" :: "num_token => i"  (\<open>#_\<close> 1000)
   "_Neg_Int" :: "num_token => i"  (\<open>#-_\<close> 1000)
 
-ML_file "Tools/numeral_syntax.ML"
+ML_file \<open>Tools/numeral_syntax.ML\<close>
 
 
 declare bin.intros [simp,TC]
@@ -698,7 +698,7 @@
   apply (simp add: zadd_ac)
   done
 
-ML_file "int_arith.ML"
+ML_file \<open>int_arith.ML\<close>
 
 subsection \<open>examples:\<close>
 
diff -r 86e8e7347ac0 -r 157990515be1 src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/Datatype.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -10,7 +10,7 @@
 keywords "datatype" "codatatype" :: thy_decl
 begin
 
-ML_file "Tools/datatype_package.ML"
+ML_file \<open>Tools/datatype_package.ML\<close>
 
 ML \<open>
 (*Typechecking rules for most datatypes involving univ*)
diff -r 86e8e7347ac0 -r 157990515be1 src/ZF/Inductive.thy
--- a/src/ZF/Inductive.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/Inductive.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -27,12 +27,12 @@
 
 lemma refl_thin: "!!P. a = a ==> P ==> P" .
 
-ML_file "ind_syntax.ML"
-ML_file "Tools/ind_cases.ML"
-ML_file "Tools/cartprod.ML"
-ML_file "Tools/inductive_package.ML"
-ML_file "Tools/induct_tacs.ML"
-ML_file "Tools/primrec_package.ML"
+ML_file \<open>ind_syntax.ML\<close>
+ML_file \<open>Tools/ind_cases.ML\<close>
+ML_file \<open>Tools/cartprod.ML\<close>
+ML_file \<open>Tools/inductive_package.ML\<close>
+ML_file \<open>Tools/induct_tacs.ML\<close>
+ML_file \<open>Tools/primrec_package.ML\<close>
 
 ML \<open>
 structure Lfp =
diff -r 86e8e7347ac0 -r 157990515be1 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/pair.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -8,7 +8,7 @@
 theory pair imports upair
 begin
 
-ML_file "simpdata.ML"
+ML_file \<open>simpdata.ML\<close>
 
 setup \<open>
   map_theory_simpset
diff -r 86e8e7347ac0 -r 157990515be1 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Sun Jan 06 12:32:01 2019 +0100
+++ b/src/ZF/upair.thy	Sun Jan 06 15:11:13 2019 +0100
@@ -16,7 +16,7 @@
 keywords "print_tcset" :: diag
 begin
 
-ML_file "Tools/typechk.ML"
+ML_file \<open>Tools/typechk.ML\<close>
 
 lemma atomize_ball [symmetric, rulify]:
      "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"