# HG changeset patch
# User wenzelm
# Date 936471678 -7200
# Node ID 7a8d3dff34b8d30fabfc3f9e0b5f15f4f211572c
# Parent  6ce03d2f7d913fe4801a096fe86c17565bef1167
ProtoPure: fake empty scope;

diff -r 6ce03d2f7d91 -r 7a8d3dff34b8 src/Pure/locale.ML
--- 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;