--- a/src/Pure/Isar/isar_thy.ML Wed Feb 03 16:50:06 1999 +0100
+++ b/src/Pure/Isar/isar_thy.ML Wed Feb 03 16:50:31 1999 +0100
@@ -241,13 +241,11 @@
fun the_theory name () = ThyInfo.theory name;
-fun begin_theory (name, names) () =
- PureThy.begin_theory name (map ThyInfo.theory names);
-
+fun begin_theory (name, names) () = ThyInfo.begin_theory name names;
fun end_theory thy =
let val thy' = PureThy.end_theory thy in
- transform_error ThyInfo.store_theory thy'
+ transform_error ThyInfo.put_theory thy'
handle exn => raise PureThy.ROLLBACK (thy', Some exn) (* FIXME !!?? *)
end;