changeset 42364 | 8c674b3b8e44 |
parent 42361 | 23f352990944 |
child 42368 | 3b8498ac2314 |
--- a/src/HOL/Decision_Procs/mir_tac.ML Sat Apr 16 16:37:21 2011 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Apr 16 18:11:20 2011 +0200 @@ -93,7 +93,7 @@ THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i) THEN (fn st => let - val g = List.nth (prems_of st, i - 1) + val g = nth (prems_of st) (i - 1) val thy = Proof_Context.theory_of ctxt (* Transform the term*) val (t,np,nh) = prepare_for_mir thy q g