equal
deleted
inserted
replaced
420 let |
420 let |
421 val thy' = Loaded_Values.put [] thy; |
421 val thy' = Loaded_Values.put [] thy; |
422 val _ = Context.set_thread_data ((SOME o Context.Theory) thy'); |
422 val _ = Context.set_thread_data ((SOME o Context.Theory) thy'); |
423 val _ = Secure.use_text notifying_context |
423 val _ = Secure.use_text notifying_context |
424 (0, Path.implode filepath) false (File.read filepath); |
424 (0, Path.implode filepath) false (File.read filepath); |
425 val thy'' = (Context.the_theory o the) (Context.thread_data ()); |
425 val thy'' = Context.the_theory (Context.the_thread_data ()); |
426 val names = Loaded_Values.get thy''; |
426 val names = Loaded_Values.get thy''; |
427 in (names, thy'') end; |
427 in (names, thy'') end; |
428 |
428 |
429 end; |
429 end; |
430 |
430 |