src/Pure/pure_thy.ML

 fun transaction f thy =
   let
     val {name, generation} = get_info thy;
     val copy_thy =
       thy
-      |> Theory.prep_ext
+      |> Theory.copy
       |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int generation)  (* FIXME !!?? *)
       |> put_info {name = name, generation = generation + 1};
     val (thy', opt_exn) = (transform_error f thy, None) handle exn => (thy, Some exn);
   in
     if Sign.is_stale (Theory.sign_of thy') then raise ROLLBACK (copy_thy, opt_exn)