simplified ThyInfo.begin_theory;
authorwenzelm
Sun, 22 Jul 2007 13:53:47 +0200
changeset 2389720ebf5cd40aa
parent 23896 26f92c405337
child 23898 461cb831d510
simplified ThyInfo.begin_theory;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Jul 22 13:53:46 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Jul 22 13:53:47 2007 +0200
     1.3 @@ -298,7 +298,7 @@
     1.4  (* init and exit *)
     1.5  
     1.6  fun begin_theory name imports uses =
     1.7 -  ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.explode) uses);
     1.8 +  ThyInfo.begin_theory name imports (map (apfst Path.explode) uses);
     1.9  
    1.10  fun end_theory thy =
    1.11    if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy;