changeset 58634 | 9f10d82e8188 |
parent 58002 | 0ed1e999a0fb |
child 58814 | 4c0ad4162cb7 |
--- a/src/HOL/Tools/coinduction.ML Wed Oct 08 14:34:30 2014 +0200 +++ b/src/HOL/Tools/coinduction.ML Wed Oct 08 17:09:07 2014 +0200 @@ -73,7 +73,7 @@ val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs |>> (fn names => Variable.variant_fixes names names_ctxt) ; val eqs = - map3 (fn name => fn T => fn (_, rhs) => + @{map 3} (fn name => fn T => fn (_, rhs) => HOLogic.mk_eq (Free (name, T), rhs)) names Ts raw_eqs; val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems