# HG changeset patch
# User wenzelm
# Date 1427239330 -3600
# Node ID a162f779925ad372f732ba73d33c98ffed345a2d
# Parent  db0b87085c168d028a394c5fc011d4c3f4a678de
dummies may depend on goal params as well;

diff -r db0b87085c16 -r a162f779925a src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Tue Mar 24 23:39:42 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Wed Mar 25 00:22:10 2015 +0100
@@ -225,11 +225,17 @@
 
     (* local fixes *)
 
-    val (fixed, fixes_ctxt) = param_ctxt
-      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes;
+    val fixes_ctxt = param_ctxt
+      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
 
     val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm mixed_insts fixes_ctxt;
 
+    fun add_fixed (Free (x, _)) =
+          if Variable.newly_fixed inst_ctxt param_ctxt x
+          then insert (op =) x else I
+      | add_fixed _ = I;
+    val fixed = fold (Term.fold_aterms add_fixed o #2) inst_vars [];
+
 
     (* lift and instantiate rule *)