--- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy Fri Oct 31 22:09:18 2014 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy Fri Oct 31 22:37:22 2014 +0100
@@ -3,10 +3,11 @@
begin
ML {*
- map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
- ["ToyList1.txt", "ToyList2.txt"]
- |> implode
- |> Thy_Info.script_thy Position.start
+ let val text =
+ map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
+ ["ToyList1.txt", "ToyList2.txt"]
+ |> implode
+ in Thy_Info.script_thy Position.start text @{theory BNF_Least_Fixpoint} end
*}
end