src/HOL/Library/refute.ML
changeset 51557 4e4b56b7a3a5
parent 50530 6266e44b3396
child 51685 385ef6706252
     1.1 --- a/src/HOL/Library/refute.ML	Wed Mar 27 17:55:21 2013 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Wed Mar 27 17:58:07 2013 +0100
     1.3 @@ -3202,6 +3202,7 @@
     1.4      "try to find a model that refutes a given subgoal"
     1.5      (scan_parms -- Scan.optional Parse.nat 1 >>
     1.6        (fn (parms, i) =>
     1.7 +        Toplevel.unknown_proof o
     1.8          Toplevel.keep (fn state =>
     1.9            let
    1.10              val ctxt = Toplevel.context_of state;