equal
deleted
inserted
replaced
61 |
61 |
62 |
62 |
63 (* retrieve info *) |
63 (* retrieve info *) |
64 |
64 |
65 fun err_not_stored name = |
65 fun err_not_stored name = |
66 error ("Theory " ^ name ^ " not stored by loader"); |
66 error ("Theory " ^ quote name ^ " not stored by loader"); |
67 |
67 |
68 fun get_thyinfo name = Symtab.lookup (! loaded_thys, name); |
68 fun get_thyinfo name = Symtab.lookup (! loaded_thys, name); |
69 |
69 |
70 fun the_thyinfo name = |
70 fun the_thyinfo name = |
71 (case get_thyinfo name of |
71 (case get_thyinfo name of |