equal
deleted
inserted
replaced
193 |
193 |
194 (** store theorems **) (*DESTRUCTIVE*) |
194 (** store theorems **) (*DESTRUCTIVE*) |
195 |
195 |
196 (* hiding -- affects current theory node only! *) |
196 (* hiding -- affects current theory node only! *) |
197 |
197 |
198 fun hide_thms b names thy = |
198 fun hide_thms fully names thy = |
199 let |
199 let |
200 val r as ref {space, thms_tab, index} = get_theorems thy; |
200 val r as ref {space, thms_tab, index} = get_theorems thy; |
201 val space' = NameSpace.hide b (space, names); |
201 val space' = NameSpace.hide fully (space, names); |
202 in r := {space = space', thms_tab = thms_tab, index = index}; thy end; |
202 in r := {space = space', thms_tab = thms_tab, index = index}; thy end; |
203 |
203 |
204 |
204 |
205 (* naming *) |
205 (* naming *) |
206 |
206 |