changeset 42364 | 8c674b3b8e44 |
parent 42361 | 23f352990944 |
child 42570 | 77f94ac04f32 |
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Apr 16 18:11:20 2011 +0200 @@ -466,7 +466,7 @@ let val (tm1,args) = strip_comb tm val adjustment = get_ty_arg_size thy tm1 val p' = if adjustment > p then p else p-adjustment - val tm_p = List.nth(args,p') + val tm_p = nth args p' handle Subscript => error ("Cannot replay Metis proof in Isabelle:\n" ^ "equality_inf: " ^ string_of_int p ^ " adj " ^