changeset 69605 | a96320074298 |
parent 67613 | ce654b0e6d69 |
--- a/src/HOL/Library/Old_Datatype.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Library/Old_Datatype.thy Sun Jan 06 15:04:34 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