# HG changeset patch
# User wenzelm
# Date 1414791442 -3600
# Node ID 4fced55fc5b7c5be0ce7b200527d426506efce5f
# Parent  2885e2eaa0fb22eb612e2f216764163e45c9e40d
provide explicit theory (amending 621c052789b4);

diff -r 2885e2eaa0fb -r 4fced55fc5b7 src/Doc/Tutorial/ToyList/ToyList_Test.thy
--- 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
diff -r 2885e2eaa0fb -r 4fced55fc5b7 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Oct 31 22:09:18 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Oct 31 22:37:22 2014 +0100
@@ -21,7 +21,7 @@
     (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
-  val script_thy: Position.T -> string -> theory
+  val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
 end;
@@ -370,9 +370,11 @@
 
 (* toplevel scripting -- without maintaining database *)
 
-fun script_thy pos txt =
+fun script_thy pos txt thy =
   let
-    val trs = Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt;
+    val trs =
+      Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt
+      |> map (Toplevel.modify_init (K thy));
     val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
     val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
   in Toplevel.end_theory end_pos end_state end;