src/Doc/Tutorial/ToyList/ToyList_Test.thy
changeset 69287 94fa3376ba33
parent 67406 23307fd33906
child 69609 ff784d5a5bfb
     1.1 --- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Sat Nov 10 19:01:20 2018 +0100
     1.2 +++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Sat Nov 10 19:39:38 2018 +0100
     1.3 @@ -4,8 +4,7 @@
     1.4  
     1.5  ML \<open>
     1.6    let val text =
     1.7 -    map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
     1.8 -      ["ToyList1.txt", "ToyList2.txt"]
     1.9 +    map (File.read o Path.append \<^master_dir>) [\<^path>\<open>ToyList1.txt\<close>, \<^path>\<open>ToyList2.txt\<close>]
    1.10      |> implode
    1.11    in Thy_Info.script_thy Position.start text @{theory} end
    1.12  \<close>