# HG changeset patch
# User wenzelm
# Date 1437906256 -7200
# Node ID 495bede1c4d9b16e3f51e1a1b90d555b9947d726
# Parent  ba81f7c40e2ae04952e691c8373f6268b26144e6
added infer_instantiate';
clarified boundary cases of instantiate';

diff -r ba81f7c40e2a -r 495bede1c4d9 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Jul 26 11:08:57 2015 +0200
+++ b/src/Pure/drule.ML	Sun Jul 26 12:24:16 2015 +0200
@@ -23,6 +23,9 @@
   val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
     thm -> thm
   val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
+  val cterm_instantiate: (cterm * cterm) list -> thm -> thm
+  val instantiate': ctyp option list -> cterm option list -> thm -> thm
+  val infer_instantiate': Proof.context -> cterm option list -> thm -> thm
   val zero_var_indexes_list: thm list -> thm list
   val zero_var_indexes: thm -> thm
   val implies_intr_hyps: thm -> thm
@@ -37,7 +40,6 @@
   val COMP: thm * thm -> thm
   val INCR_COMP: thm * thm -> thm
   val COMP_INCR: thm * thm -> thm
-  val cterm_instantiate: (cterm * cterm) list -> thm -> thm
   val size_of_thm: thm -> int
   val reflexive_thm: thm
   val symmetric_thm: thm
@@ -47,7 +49,6 @@
   val cut_rl: thm
   val revcut_rl: thm
   val thin_rl: thm
-  val instantiate': ctyp option list -> cterm option list -> thm -> thm
 end;
 
 signature DRULE =
@@ -842,14 +843,18 @@
         err "more instantiations than variables in thm";
 
     val thm' =
-      if forall is_none cTs then thm
-      else
-        Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
+      Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
     val thm'' =
-      if forall is_none cts then thm'
-      else
-        Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
-    in thm'' end;
+      Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
+  in thm'' end;
+
+fun infer_instantiate' ctxt args th =
+  let
+    val vars = rev (Term.add_var_names (Thm.full_prop_of th) []);
+    val args' = zip_options vars args
+      handle ListPair.UnequalLengths =>
+        raise THM ("infer_instantiate': more instantiations than variables in thm", 0, [th]);
+  in infer_instantiate ctxt args' th end;