--- a/src/Tools/coherent.ML Sun Jul 26 13:12:53 2009 +0200
+++ b/src/Tools/coherent.ML Sun Jul 26 13:12:54 2009 +0200
@@ -215,7 +215,7 @@
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
SUBPROOF (fn {prems = prems', concl, context, ...} =>
- let val xs = map term_of params @
+ let val xs = map (term_of o #2) params @
map (fn (_, s) => Free (s, the (Variable.default_type context s)))
(Variable.fixes_of context)
in