src/Provers/trancl.ML

--- a/src/Provers/trancl.ML	Sat Apr 16 16:37:21 2011 +0200
+++ b/src/Provers/trancl.ML	Sat Apr 16 18:11:20 2011 +0200
@@ -95,8 +95,8 @@
     fun inst thm =
       let val SOME (_, _, r', _) = decomp (concl_of thm)
       in Drule.cterm_instantiate [(cterm_of thy r', cterm_of thy r)] thm end;
-    fun pr (Asm i) = List.nth (asms, i)
-      | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm
+    fun pr (Asm i) = nth asms i
+      | pr (Thm (prfs, thm)) = map pr prfs MRS inst thm;
   in pr end;