src/Tools/coherent.ML
changeset 32199 82c4c570310a
parent 32091 30e2ffbba718
child 32734 06c13b2e562e
     1.1 --- a/src/Tools/coherent.ML	Sun Jul 26 13:12:53 2009 +0200
     1.2 +++ b/src/Tools/coherent.ML	Sun Jul 26 13:12:54 2009 +0200
     1.3 @@ -215,7 +215,7 @@
     1.4  fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
     1.5    rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
     1.6    SUBPROOF (fn {prems = prems', concl, context, ...} =>
     1.7 -    let val xs = map term_of params @
     1.8 +    let val xs = map (term_of o #2) params @
     1.9        map (fn (_, s) => Free (s, the (Variable.default_type context s)))
    1.10          (Variable.fixes_of context)
    1.11      in