diff -r df0cb410be35 -r 128459bd72d2 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Dec 01 16:02:57 2008 +0100
+++ b/src/Pure/facts.ML	Mon Dec 01 19:41:16 2008 +0100
@@ -192,7 +192,7 @@
 
 fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
   let
-    val (name, facts') = if Name.is_nothing b then ("", facts)
+    val (name, facts') = if Binding.is_nothing b then ("", facts)
       else let
         val (space, tab) = facts;
         val (name, space') = NameSpace.declare_binding naming b space;