SeLFiE: Print_Is_Free, Print_Is_Var, Print_Is_Bound does not work for variables with question marks.

[yutakang]

In Hybrid_Logic.thy,

ML‹
try (Syntax.read_term @{context}) "?g"
›
lemma soundness': ‹n ⊢ branch ⟹ M, g ⊨⇩Θ branch ⟹ False›(!)
assert_SeLFiE_true generalize_arguments_used_in_recursion_deep [on["branch"], arb["g"], rule["ST.induct"]]
assert_SeLFiE_false generalize_arguments_used_in_recursion_deep [on["branch"], arb[ ], rule["ST.induct"]]

It was caused by is_variable.

[yutakang]

I am not sure what the right fix would be to this issue.

• Should I remove the question marks?
• Should I avoid using Is_Free, Is_Bound, Is_Var at least for inner cases?