more precise context -- potentially relevant for Eisbach dummy thm;

--- a/src/Pure/Tools/rule_insts.ML	Thu Dec 31 15:26:14 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Thu Dec 31 15:27:25 2015 +0100
@@ -114,7 +114,8 @@
 
     (*eigen-context*)
     val (_, ctxt1) = ctxt
-      |> Variable.declare_thm thm
+      |> fold (Variable.declare_internal o Logic.mk_type o TVar) tvars
+      |> fold (Variable.declare_internal o Var) vars
       |> Proof_Context.add_fixes_cmd raw_fixes;
 
     (*explicit type instantiations*)

--- a/src/Pure/variable.ML	Thu Dec 31 15:26:14 2015 +0100
+++ b/src/Pure/variable.ML	Thu Dec 31 15:27:25 2015 +0100
@@ -18,6 +18,7 @@
   val declare_maxidx: int -> Proof.context -> Proof.context
   val declare_names: term -> Proof.context -> Proof.context
   val declare_constraints: term -> Proof.context -> Proof.context
+  val declare_internal: term -> Proof.context -> Proof.context
   val declare_term: term -> Proof.context -> Proof.context
   val declare_typ: typ -> Proof.context -> Proof.context
   val declare_prf: Proofterm.proof -> Proof.context -> Proof.context