# HG changeset patch
# User wenzelm
# Date 1470995676 -7200
# Node ID eb4f59275c05d62cf9bbc422538805483a0f700c
# Parent  8e0148e1f5f49dfd635911ccbeaf56df2393191f
liberal name as in document antiquotations;

diff -r 8e0148e1f5f4 -r eb4f59275c05 src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Fri Aug 12 11:53:47 2016 +0200
+++ b/src/Doc/Implementation/Integration.thy	Fri Aug 12 11:54:36 2016 +0200
@@ -132,7 +132,7 @@
 \<close>
 
 text %mlex \<open>
-  The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example Isar
+  The file @{file "~~/src/HOL/ex/Commands.thy"} shows some example Isar
   command definitions, with the all-important theory header declarations for
   outer syntax keywords.
 \<close>
diff -r 8e0148e1f5f4 -r eb4f59275c05 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Aug 12 11:53:47 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Aug 12 11:54:36 2016 +0200
@@ -199,10 +199,10 @@
 (** invocation of Haskell interpreter **)
 
 val narrowing_engine =
-  File.read @{"file" "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
+  File.read @{file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
 
 val pnf_narrowing_engine =
-  File.read @{"file" "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
+  File.read @{file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
 
 fun exec verbose code =
   ML_Context.exec (fn () =>
diff -r 8e0148e1f5f4 -r eb4f59275c05 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Fri Aug 12 11:53:47 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Aug 12 11:54:36 2016 +0200
@@ -96,7 +96,7 @@
 local
 
 val antiq =
-  Parse.!!! ((Parse.token Parse.name ::: Parse.args) --| Scan.ahead Parse.eof);
+  Parse.!!! ((Parse.token Parse.liberal_name ::: Parse.args) --| Scan.ahead Parse.eof);
 
 fun make_env name visible =
   (ML_Lex.tokenize