1.1 --- a/src/Pure/Isar/toplevel.ML	Sat May 15 22:24:25 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat May 15 23:16:32 2010 +0200
     1.3 @@ -660,8 +660,8 @@
     1.4    let val st' = command tr st in
     1.5      if immediate orelse
     1.6        null proof_trs orelse
     1.7 -      OuterKeyword.is_schematic_goal (name_of tr) orelse
     1.8 -      exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse
     1.9 +      Keyword.is_schematic_goal (name_of tr) orelse
    1.10 +      exists (Keyword.is_qed_global o name_of) proof_trs orelse
    1.11        not (can proof_of st') orelse
    1.12        Proof.is_relevant (proof_of st')
    1.13      then