# HG changeset patch
# User wenzelm
# Date 1451572045 -3600
# Node ID 12d3edd62932090cb0382f9762fe0186c001fd7e
# Parent  03e69b1bf359a7f8d9819a042c761d1d9a3246e1
more precise context -- potentially relevant for Eisbach dummy thm;

diff -r 03e69b1bf359 -r 12d3edd62932 src/Pure/Tools/rule_insts.ML
--- 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*)
diff -r 03e69b1bf359 -r 12d3edd62932 src/Pure/variable.ML
--- 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