author | wenzelm |
Sat, 04 Sep 1999 21:01:18 +0200 | |
changeset 7469 | 7a8d3dff34b8 |
parent 7468 | 6ce03d2f7d91 |
child 7470 | 9f67ca1e03dc |
--- a/src/Pure/locale.ML Sat Sep 04 21:00:20 1999 +0200 +++ b/src/Pure/locale.ML Sat Sep 04 21:01:18 1999 +0200 @@ -160,7 +160,9 @@ (* access scope *) -val get_scope_sg = ! o #scope o LocalesData.get_sg; +fun get_scope_sg sg = + if Sign.eq_sg (sg, Theory.sign_of ProtoPure.thy) then [] + else ! (#scope (LocalesData.get_sg sg)); val get_scope = get_scope_sg o Theory.sign_of;