src/Tools/coherent.ML
changeset 32199 82c4c570310a
parent 32091 30e2ffbba718
child 32734 06c13b2e562e
--- 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