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