src/Pure/pure_thy.ML
changeset 5026 9a67a024f4b8
parent 5022 b4bd7e6402fe
child 5041 a1d0a6d555cd
equal deleted inserted replaced
5025:fc1a2421800f 5026:9a67a024f4b8
   340     val copy_thy =
   340     val copy_thy =
   341       thy
   341       thy
   342       |> Theory.prep_ext
   342       |> Theory.prep_ext
   343       |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int generation)  (* FIXME !!?? *)
   343       |> Theory.add_name ("#" ^ name ^ ":" ^ string_of_int generation)  (* FIXME !!?? *)
   344       |> put_info {name = name, generation = generation + 1};
   344       |> put_info {name = name, generation = generation + 1};
       
   345     val (thy', opt_exn) = (transform_error f thy, None) handle exn => (thy, Some exn);
   345   in
   346   in
   346     (transform_error f thy, false, None) handle exn =>
   347     if Sign.is_stale (Theory.sign_of thy') then
   347       if Sign.is_stale (Theory.sign_of thy) then (copy_thy, true, Some exn)
   348       (copy_thy, true, opt_exn)
   348       else (thy, false, Some exn)
   349     else (thy', false, opt_exn)
   349   end;
   350   end;
   350 
   351 
   351 
   352 
   352 
   353 
   353 (** add logical types **)
   354 (** add logical types **)