src/Pure/facts.ML
changeset 26290 e025bf1cc0f1
parent 26281 328fd1c551ef
child 26307 27d3de85c266
     1.1 --- a/src/Pure/facts.ML	Sat Mar 15 22:07:29 2008 +0100
     1.2 +++ b/src/Pure/facts.ML	Sat Mar 15 22:07:31 2008 +0100
     1.3 @@ -77,6 +77,9 @@
     1.4    in make_facts facts' props' end;
     1.5  
     1.6  fun del name (Facts {facts = (space, tab), props}) =
     1.7 -  make_facts (space, Symtab.delete_safe name tab) props;
     1.8 +  let
     1.9 +    val space' = NameSpace.hide true name space handle ERROR _ => space;
    1.10 +    val tab' = Symtab.delete_safe name tab;
    1.11 +  in make_facts (space', tab') props end;
    1.12  
    1.13  end;