1.1 --- a/src/Pure/pure_thy.ML	Mon Dec 01 16:02:57 2008 +0100
     1.2 +++ b/src/Pure/pure_thy.ML	Mon Dec 01 19:41:16 2008 +0100
     1.3 @@ -144,7 +144,7 @@
     1.4    (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
     1.5  
     1.6  fun enter_thms pre_name post_name app_att (b, thms) thy =
     1.7 -  if Name.is_nothing b
     1.8 +  if Binding.is_nothing b
     1.9    then swap (enter_proofs (app_att (thy, thms)))
    1.10    else let
    1.11      val naming = Sign.naming_of thy;
    1.12 @@ -198,7 +198,7 @@
    1.13  
    1.14  fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
    1.15    let
    1.16 -    val pos = Name.pos_of b;
    1.17 +    val pos = Binding.pos_of b;
    1.18      val name = Sign.full_binding thy b;
    1.19      val _ = Position.report (Markup.fact_decl name) pos;
    1.20