src/Pure/Thy/thy_info.ML
changeset 9953 035a8288310a
parent 9822 dcf5f9886b8f
child 10009 45c1eb3d8ad4
equal deleted inserted replaced
9952:24914e42b857 9953:035a8288310a
   383 
   383 
   384 fun begin_theory present upd name parents paths =
   384 fun begin_theory present upd name parents paths =
   385   let
   385   let
   386     val assert_thy = if upd then quiet_update_thy true else weak_use_thy;
   386     val assert_thy = if upd then quiet_update_thy true else weak_use_thy;
   387     val _ = check_unfinished error name;
   387     val _ = check_unfinished error name;
       
   388     val _ = priority (loader_msg "looking up" [name]);
   388     val _ = (map Path.basic parents; seq assert_thy parents);
   389     val _ = (map Path.basic parents; seq assert_thy parents);
   389     val theory = PureThy.begin_theory name (map get_theory parents);
   390     val theory = PureThy.begin_theory name (map get_theory parents);
   390     val deps =
   391     val deps =
   391       if known_thy name then get_deps name
   392       if known_thy name then get_deps name
   392       else (init_deps None (map #1 paths));   (*records additional ML files only!*)
   393       else (init_deps None (map #1 paths));   (*records additional ML files only!*)