more robust (amending 1600fb749c54), to support the following corner case:
schematic_goal "PROP ((?f :: ?'a \<Rightarrow> _) (x :: ?'a))"
apply (tactic \<open>PRIMITIVE (Thm.instantiate (TVars.make1 ((("'a", 0), []), @{ctyp prop}), Vars.empty))\<close>)
oops