changeset 27575 | e540ad3fb50a |
parent 27439 | 7d5c4e73c89e |
child 27614 | f38c25d106a7 |
--- a/src/Pure/Isar/outer_syntax.ML Mon Jul 14 17:51:41 2008 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Mon Jul 14 17:51:42 2008 +0200 @@ -202,7 +202,7 @@ let val result = ref thy; val trs = parse (Path.position path) (File.read path); - val init = Toplevel.init_theory "" (K thy) (fn thy' => result := thy') (K ()); + val init = Toplevel.init_theory "" (K thy) (fn thy' => result := thy'); val _ = Toplevel.excursion (init Toplevel.empty :: trs @ [Toplevel.exit Toplevel.empty]); in ! result end;