(** Applying HypsubstFun to generate hyp_subst_tac **)
structure Hypsubst_Data =
struct
structure Simplifier = Simplifier
fun dest_eq (Const("op =",T) $ t $ u) = ((t, u), domain_type T)
val dest_Trueprop = FOLogic.dest_Trueprop
val dest_imp = FOLogic.dest_imp
val eq_reflection = eq_reflection
val rev_eq_reflection = meta_eq_to_obj_eq
val imp_intr = impI
val rev_mp = rev_mp
val subst = subst
val sym = sym
val thin_refl = prove_goal (the_context ()) "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
end;
structure Hypsubst = HypsubstFun(Hypsubst_Data);
open Hypsubst;