--- a/src/Pure/Isar/isar_cmd.ML Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sat Oct 24 19:47:37 2009 +0200
@@ -400,7 +400,7 @@
val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
val {classes, ...} = Sorts.rep_algebra algebra;
fun entry (c, (i, (_, cs))) =
- (i, {name = NameSpace.extern space c, ID = c, parents = cs,
+ (i, {name = Name_Space.extern space c, ID = c, parents = cs,
dir = "", unfold = true, path = ""});
val gr =
Graph.fold (cons o entry) classes []