[isabelle] tactic being executed twice




Hi,

I have a (part) theory file, with goal and tactic as follows

theory Scratch imports ZF begin
lemma oracle_test: "A ⟶ A & B"
  apply (rule impI)
  apply (rule conjI)
apply (tactic {* fn thm =>
  let
    val _ = writeln "aaa" ;
    val _ = writeln (@{make_string} thm) ;
    val cps = Drule.cprems_of thm ;
    val _ = writeln "ccc" ;
    val _ = writeln (@{make_string} cps) ;
    val _ = writeln "ddd" ;
  in Seq.succeed thm end ; *})

At this point it seems clear that the tactic is executed twice, the first time seemingly with an argument thm which gets printed out as "TERM _", and the second time with the actual goal state.

Why is this? What's going on here? Is this how apply tactic ... should be used?

Thanks

Jeremy




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