src/Pure/Thy/thy_load.ML
changeset 6978 a5b67157b94d
parent 6641 254ab03bd082
child 7190 ba6f09cd7769
equal deleted inserted replaced
6977:4781c0673e83 6978:a5b67157b94d
    79 
    79 
    80 
    80 
    81 (* check_thy *)
    81 (* check_thy *)
    82 
    82 
    83 fun tmp_path path f x =
    83 fun tmp_path path f x =
    84   if Path.is_current path then f x else Library.setmp load_path [path] f x;
    84   if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
    85 
    85 
    86 fun check_thy_aux name ml =
    86 fun check_thy_aux name ml =
    87   (case check_file (thy_path name) of
    87   (case check_file (thy_path name) of
    88     None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
    88     None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
    89       commas_quote (show_path ()))
    89       commas_quote (show_path ()))