ThyInfo.begin_theory;
authorwenzelm
Wed Feb 03 16:50:31 1999 +0100 (1999-02-03 ago)
changeset 61987fa2deb92b39
parent 6197 4328d436c556
child 6199 9b1be867e21a
ThyInfo.begin_theory;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Feb 03 16:50:06 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Feb 03 16:50:31 1999 +0100
     1.3 @@ -241,13 +241,11 @@
     1.4  
     1.5  fun the_theory name () = ThyInfo.theory name;
     1.6  
     1.7 -fun begin_theory (name, names) () =
     1.8 -  PureThy.begin_theory name (map ThyInfo.theory names);
     1.9 -
    1.10 +fun begin_theory (name, names) () = ThyInfo.begin_theory name names;
    1.11  
    1.12  fun end_theory thy =
    1.13    let val thy' = PureThy.end_theory thy in
    1.14 -    transform_error ThyInfo.store_theory thy'
    1.15 +    transform_error ThyInfo.put_theory thy'
    1.16        handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)
    1.17    end;
    1.18