changeset 60094 | 96a4765ba7d1 |
parent 59936 | b8ffc3dc9e24 |
child 60190 | 906de96ba68a |
--- a/src/HOL/Library/refute.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/HOL/Library/refute.ML Thu Apr 16 14:18:32 2015 +0200 @@ -2969,7 +2969,6 @@ "try to find a model that refutes a given subgoal" (scan_parms -- Scan.optional Parse.nat 1 >> (fn (parms, i) => - Toplevel.unknown_proof o Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state;