diff -r b96cf915de75 -r 9a2c266f97c8 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Apr 03 12:49:13 2017 +0200 +++ b/src/Pure/PIDE/document.ML Mon Apr 03 13:39:13 2017 +0200 @@ -178,9 +178,7 @@ | NONE => false); fun loaded_theory name = - (case try (unsuffix ".thy") name of - SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a] - | NONE => NONE); + get_first Thy_Info.lookup_theory [name, Long_Name.base_name name]; fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node;