src/Pure/pure_thy.ML
changeset 6350 b5f1f861155d
parent 6094 fd0f737b1956
child 6367 7f36b6fd3eb3
equal deleted inserted replaced
6349:f7750d816c21 6350:b5f1f861155d
   219 fun warn_same name =
   219 fun warn_same name =
   220   cond_warning name ("Theorem database already contains a copy of " ^ quote name);
   220   cond_warning name ("Theorem database already contains a copy of " ^ quote name);
   221 
   221 
   222 fun enter_thmx sg app_name (bname, thmx) =
   222 fun enter_thmx sg app_name (bname, thmx) =
   223   let
   223   let
   224     val name = Sign.full_name sg bname;
   224     val name = Sign.full_name sg (default_name bname);
   225     val named_thms = map Thm.name_thm (app_name name thmx);
   225     val named_thms = map Thm.name_thm (app_name name thmx);
   226 
   226 
   227     val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
   227     val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
   228 
   228 
   229     val overwrite =
   229     val overwrite =