[isabelle] tactic being executed twice


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 =>
    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?



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