# HG changeset patch
# User wenzelm
# Date 1185105227 -7200
# Node ID 20ebf5cd40aa6cffab5baba28b7a5a95e49275a4
# Parent  26f92c40533745e7489a8b894c405b912f5c0199
simplified ThyInfo.begin_theory;

diff -r 26f92c405337 -r 20ebf5cd40aa src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Jul 22 13:53:46 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Jul 22 13:53:47 2007 +0200
@@ -298,7 +298,7 @@
 (* init and exit *)
 
 fun begin_theory name imports uses =
-  ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.explode) uses);
+  ThyInfo.begin_theory name imports (map (apfst Path.explode) uses);
 
 fun end_theory thy =
   if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy;