src/Pure/facts.ML
changeset 28941 128459bd72d2
parent 28864 d6fe93e3dcb9
child 28965 1de908189869
     1.1 --- a/src/Pure/facts.ML	Mon Dec 01 16:02:57 2008 +0100
     1.2 +++ b/src/Pure/facts.ML	Mon Dec 01 19:41:16 2008 +0100
     1.3 @@ -192,7 +192,7 @@
     1.4  
     1.5  fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
     1.6    let
     1.7 -    val (name, facts') = if Name.is_nothing b then ("", facts)
     1.8 +    val (name, facts') = if Binding.is_nothing b then ("", facts)
     1.9        else let
    1.10          val (space, tab) = facts;
    1.11          val (name, space') = NameSpace.declare_binding naming b space;