changeset 21621 | f9fd69d96c4e |
parent 21078 | 101aefd61aac |
child 21669 | c68717c16013 |
--- a/src/HOL/ex/reflection.ML Fri Dec 01 17:22:30 2006 +0100 +++ b/src/HOL/ex/reflection.ML Fri Dec 01 17:22:31 2006 +0100 @@ -190,7 +190,7 @@ (AList.delete (op =) (xn,0) tml) val th = (instantiate ([], - [(cert vs, cvs),(cert n, t' |> index_of |> HOLogic.mk_nat |> cert)] + [(cert vs, cvs),(cert n, t' |> index_of |> IntInf.fromInt |> HOLogic.mk_nat |> cert)] @cts) eq) RS sym in hd (Variable.export ctxt' ctxt [th]) end)