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*)