simplified ThyInfo.begin_theory;
authorwenzelm
Sun, 22 Jul 2007 13:53:47 +0200
changeset 23897 20ebf5cd40aa
parent 23896 26f92c405337
child 23898 461cb831d510
simplified ThyInfo.begin_theory;
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;