equal
deleted
inserted
replaced
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 ())) |