# HG changeset patch
# User wenzelm
# Date 1444143434 -7200
# Node ID 93883c8250625f9ce84f5810e288343f7087dc4a
# Parent  de610e8df459caad44b29040b40d63b875d782ac
added Thm.forall_intr_name;

diff -r de610e8df459 -r 93883c825062 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Oct 06 15:39:00 2015 +0200
+++ b/src/Pure/more_thm.ML	Tue Oct 06 16:57:14 2015 +0200
@@ -64,6 +64,7 @@
   val undeclared_hyps: Context.generic -> thm -> term list
   val check_hyps: Context.generic -> thm -> thm
   val elim_implies: thm -> thm -> thm
+  val forall_intr_name: string * cterm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
   val instantiate': ctyp option list -> cterm option list -> thm -> thm
@@ -319,6 +320,15 @@
 fun elim_implies thA thAB = Thm.implies_elim thAB thA;
 
 
+(* forall_intr_name *)
+
+fun forall_intr_name (a, x) th =
+  let
+    val th' = Thm.forall_intr x th;
+    val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b));
+  in Thm.renamed_prop prop' th' end;
+
+
 (* forall_elim_var(s) *)
 
 local