src/Pure/Isar/toplevel.ML
changeset 51274 cfc83ad52571
parent 51273 d54ee0cad2ab
child 51278 1ee77b36490e
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:52:27 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Feb 25 13:29:19 2013 +0100
     1.3 @@ -720,8 +720,7 @@
     1.4      val st' = command head_tr st;
     1.5    in
     1.6      if not future_enabled orelse is_ignored head_tr orelse
     1.7 -      Keyword.is_schematic_goal (name_of head_tr) orelse null proof_trs orelse
     1.8 -      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     1.9 +      null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st')
    1.10      then
    1.11        let val (results, st'') = fold_map atom_result proof_trs st'
    1.12        in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end