# HG changeset patch # User wenzelm # Date 918057031 -3600 # Node ID 7fa2deb92b39e95fe266d8aafed4b2e3a9017829 # Parent 4328d436c556bfee8582ee0d34300da57eb9cc9a ThyInfo.begin_theory; diff -r 4328d436c556 -r 7fa2deb92b39 src/Pure/Isar/isar_thy.ML --- 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;