diff -r 7e2c8a63a8f8 -r 2da59cdf531c src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Sat Jul 25 23:15:37 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML	Sat Jul 25 23:41:53 2015 +0200
@@ -175,8 +175,7 @@
   val PROVE_HYP: thm -> thm -> thm
 
   val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
-  val EXISTS: cterm * cterm -> thm -> thm
-  val EXISTL: cterm list -> thm -> thm
+  val EXISTS: Proof.context -> cterm * cterm -> thm -> thm
   val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
 
   val EVEN_ORS: thm list -> thm list
@@ -1199,29 +1198,11 @@
       handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
   end;
 
-local
-  val prop = Thm.prop_of exI
-  val [P, x] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars prop)
-in
-fun EXISTS (template,witness) thm =
+fun EXISTS ctxt (template,witness) thm =
   let val abstr = #2 (Dcterm.dest_comb template) in
-    thm RS (cterm_instantiate [(P, abstr), (x, witness)] exI)
+    thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI)
       handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
-  end
-end;
-
-(*----------------------------------------------------------------------------
- *
- *         A |- M
- *   -------------------   [v_1,...,v_n]
- *    A |- ?v1...v_n. M
- *
- *---------------------------------------------------------------------------*)
-
-fun EXISTL vlist th =
-  fold_rev (fn v => fn thm => EXISTS(Dcterm.mk_exists(v,cconcl thm), v) thm)
-           vlist th;
-
+  end;
 
 (*----------------------------------------------------------------------------
  *
@@ -1238,7 +1219,7 @@
     fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
   in
     fold_rev (fn (b as (r1,r2)) => fn thm =>
-        EXISTS(ex r2 (subst_free [b]
+        EXISTS ctxt (ex r2 (subst_free [b]
                    (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
               thm)
        blist' th
@@ -1453,13 +1434,7 @@
 
 fun PGEN ctxt tych a vstr th =
   let val a1 = tych a
-      val vstr1 = tych vstr
-  in
-  Thm.forall_intr a1
-     (if (is_Free vstr)
-      then cterm_instantiate [(vstr1,a1)] th
-      else VSTRUCT_ELIM ctxt tych a vstr th)
-  end;
+  in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end;
 
 
 (*---------------------------------------------------------------------------
@@ -2243,7 +2218,7 @@
      val a = Free (aname, T)
      val v = Free (vname, T)
      val a_eq_v = HOLogic.mk_eq(a,v)
-     val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
+     val ex_th0 = Rules.EXISTS ctxt (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
                            (Rules.REFL (tych a))
      val th0 = Rules.ASSUME (tych a_eq_v)
      val rows = map (fn x => ([x], (th0,[]))) pats