# HG changeset patch
# User wenzelm
# Date 1568640638 -7200
# Node ID 91319c3d28415691d6e10628de60ef740604a9a5
# Parent  3f557ed88fd64b3ee0ede275f04b0dae9c4b498f
tuned;

diff -r 3f557ed88fd6 -r 91319c3d2841 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Sep 16 12:03:25 2019 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Sep 16 15:30:38 2019 +0200
@@ -370,7 +370,7 @@
     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
   end;
 
-fun check_deps dir name =
+fun check_thy_deps dir name =
   (case lookup_deps name of
     SOME NONE => (true, NONE, Position.none, get_imports name, [])
   | NONE =>
@@ -402,7 +402,7 @@
         let
           val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
 
-          val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name
+          val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name
             handle ERROR msg =>
               cat_error msg
                 ("The error(s) above occurred for theory " ^ quote theory_name ^