Theory.hide_space_i true;
authorwenzelm
Fri, 21 Dec 2001 23:17:35 +0100
changeset 12589afc6ffffeb11
parent 12588 0361fd72f1a7
child 12590 3573830e9b91
Theory.hide_space_i true;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Dec 21 23:17:12 2001 +0100
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Dec 21 23:17:35 2001 +0100
     1.3 @@ -250,7 +250,7 @@
     1.4          val names = map (intern sg kind) xnames;
     1.5          val bads = filter_out (check sg) names;
     1.6        in
     1.7 -        if null bads then Theory.hide_space_i (kind, names) thy
     1.8 +        if null bads then Theory.hide_space_i true (kind, names) thy
     1.9          else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
    1.10        end
    1.11    | None => error ("Bad name space specification: " ^ quote kind));