equal
deleted
inserted
replaced
54 setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x; |
54 setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x; |
55 |
55 |
56 fun pass_theory thy f x = |
56 fun pass_theory thy f x = |
57 (case pass (Some thy) f x of |
57 (case pass (Some thy) f x of |
58 (y, Some thy') => (y, thy') |
58 (y, Some thy') => (y, thy') |
59 | (_, None) => error "Missing ML theory context"); |
59 | (_, None) => error "Lost theory context in ML"); |
60 |
60 |
61 fun save f x = setmp (get_context ()) f x; |
61 fun save f x = setmp (get_context ()) f x; |
62 |
62 |
63 |
63 |
64 (* map context *) |
64 (* map context *) |