# [isabelle] emergence of "TERM _" (using quickcheck and nitpick)

I'm getting exceptions and having other kinds of problems when using
quickcheck or nitpick inside tactics. I define a tactic that should fail
when quickcheck finds a counterexample and shouldn't do anything otherwise,
as follows:
fun check_counter_tac ctxt thm =
let
val term = concl_of thm
in
case Quickcheck.test_terms ctxt (true, true) [] [(term, [])] of
NONE => Seq.single thm
| _ => Seq.empty
end;
Then I try to run the tactic in a proof, like this:
lemma "0=(1::nat)" apply (tactic "check_counter_tac @{context}")
but I get the following exception:
exception TYPE raised (line 273 of "sign.ML"):
Type error in application: incompatible operand type
Operator: If :: bool => (bool × term list) option => (bool × term list)
option => (bool × term list) option
Operand: TERM _ :: prop
bool => (bool × term list) option => (bool × term list) option => (bool ×
term list) option
prop
If
TERM _
The function Quickcheck.test_terms works fine otherwise, e.g., if I feed it
a term manually, or if I feed it the goal directly inside ML_val{**}.
I'm having the same problem when trying to use nitpick inside a tactic. I
don't get the exception, but it seems that the tactic is feeding the
nitpick function the same dummy term TERM _, and nitpick will never find a
counterexample. It writes:
Nitpicking goal:
TERM _.
and finds nothing.
Does anyone know what this is about?
Thanks,
Daniel

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*