diff -r 39cc38a06610 -r a2fa0c6a7aff src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Nov 27 16:57:34 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Tue Nov 28 22:14:10 2017 +0100
@@ -108,26 +108,24 @@
   | NONE => Long_Name.qualifier theory);
 
 fun theory_name qualifier theory =
-  if loaded_theory theory then (true, theory)
-  else
-    let val theory' =
-      if Long_Name.is_qualified theory orelse is_some (global_theory theory)
-      then theory
-      else Long_Name.qualify qualifier theory
-    in (false, theory') end;
+  if Long_Name.is_qualified theory orelse is_some (global_theory theory)
+  then theory
+  else Long_Name.qualify qualifier theory;
 
 fun import_name qualifier dir s =
-  (case theory_name qualifier (Thy_Header.import_name s) of
-    (true, theory) => {master_dir = Path.current, theory_name = theory}
-  | (false, theory) =>
-      let val node_name =
-        (case known_theory theory of
-          SOME node_name => node_name
-        | NONE =>
-            if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
-            then Path.explode s
-            else File.full_path dir (thy_path (Path.expand (Path.explode s))))
-      in {master_dir = Path.dir node_name, theory_name = theory} end);
+  let val theory = theory_name qualifier (Thy_Header.import_name s) in
+    if loaded_theory theory then {master_dir = Path.current, theory_name = theory}
+    else
+      let
+        val node_name =
+          (case known_theory theory of
+            SOME node_name => node_name
+          | NONE =>
+              if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
+              then Path.explode s
+              else File.full_path dir (thy_path (Path.expand (Path.explode s))));
+      in {master_dir = Path.dir node_name, theory_name = theory} end
+  end;
 
 fun check_file dir file = File.check_file (File.full_path dir file);