src/Pure/Isar/toplevel.ML
changeset 36315 e859879079c8
parent 35205 611b90bb89bc
child 36355 aaa9933039b3
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Apr 23 19:36:23 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Apr 23 21:00:28 2010 +0200
     1.3 @@ -658,8 +658,11 @@
     1.4  
     1.5  fun proof_result immediate (tr, proof_trs) st =
     1.6    let val st' = command tr st in
     1.7 -    if immediate orelse null proof_trs orelse
     1.8 -      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     1.9 +    if immediate orelse
    1.10 +      null proof_trs orelse
    1.11 +      OuterKeyword.is_schematic_goal (name_of tr) orelse
    1.12 +      not (can proof_of st') orelse
    1.13 +      Proof.is_relevant (proof_of st')
    1.14      then
    1.15        let val (states, st'') = fold_map command_result proof_trs st'
    1.16        in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end