moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
* * *
made example compile again
theory ToyList_Test
imports BNF_Least_Fixpoint
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
*}
end