src/Pure/Thy/thy_read.ML
changeset 1244 3d408455d69f
parent 1242 b3f68a644380
child 1262 8f40ff1299d8
equal deleted inserted replaced
1243:fa09705a5890 1244:3d408455d69f
   356 
   356 
   357           update_simps (None,
   357           update_simps (None,
   358             Some (gen_rems same_thm (#simps(rep_ss (!simpset)), !old_simps)))
   358             Some (gen_rems same_thm (#simps(rep_ss (!simpset)), !old_simps)))
   359          );
   359          );
   360 
   360 
   361        (*Store theory again because it could have been redefined*)
   361          use_string
   362        use_string
   362            ["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");\
   363          ["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ "); " ^
   363             \map store_thm_db (axioms_of " ^ tname ^ ".thy));"];
   364 
   364                     (*Store theory again because it could have been redefined*)
   365        (*Store new axioms in theorem database; ignore theories which are just
       
   366          copies of existing ones*)
       
   367        let val parents = get_parents tname;
       
   368            val fst_thy = get_theory (hd parents);
       
   369            val this_thy = get_theory tname;
       
   370        in if length parents = 1
       
   371              andalso Sign.eq_sg (sign_of fst_thy, sign_of this_thy) then ""
       
   372           else
       
   373             "map store_thm_db (axioms_of " ^ tname ^ ".thy));"
       
   374        end];
       
   375 
   365 
   376        (*Now set the correct info*)
   366        (*Now set the correct info*)
   377        set_info (Some (file_info thy_file)) (Some (file_info ml_file)) tname;
   367        set_info (Some (file_info thy_file)) (Some (file_info ml_file)) tname;
   378        set_path ();
   368        set_path ();
   379 
   369