theory Odd_Failure
imports HOL
begin

typedecl nat

consts
  P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
  Q :: "nat \<Rightarrow> bool"

lemma R: (* triggers the error *)
  fixes s t :: nat assumes "P s t"
  shows "\<forall>(s::nat) (t::nat). Q t" sorry

lemma R2: (* works as expected, with (unused) bound variable renamed. *)
  fixes s t :: nat assumes "P s t"
  shows "\<forall>(s'::nat) (t::nat). Q t" sorry

(* both rules are alpha-equivalent: *)

ML {*
  (op aconv o pairself prop_of) (@{thm R}, @{thm R2})
*}

lemma "\<And>(a::nat) (b::nat). P a b \<Longrightarrow> \<forall>(c::nat) (c::nat). Q c"
    apply (rule R) (* wrong step here *)
    (*apply assumption*) (* fails here *)
    oops


text {* The same thing in ML without any Isar management: *}

ML {*
  let
    val goal = @{cprop "\<And>(a::nat) (b::nat). P a b \<Longrightarrow> \<forall>(c::nat) (c::nat). Q c"}
    val rule = @{thm R}
    val st = Goal.init goal
  in
    st |> rtac rule 1 |> Seq.hd
  end
*}
