# HG changeset patch
# User obua
# Date 1140056637 -3600
# Node ID df24f2564aaa065dfc785c649c0626eb8f3b2a5d
# Parent  82e2d66f995bcd77a216bcef08beb6428086f542
adapted to kernel changes

diff -r 82e2d66f995b -r df24f2564aaa src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Feb 16 00:09:46 2006 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Thu Feb 16 03:23:57 2006 +0100
@@ -1053,9 +1053,9 @@
 fun rearrange sg tm th =
     let
 	val tm' = Envir.beta_eta_contract tm
-	fun find []      n = permute_prems 0 1 0 (implies_intr (Thm.cterm_of sg tm) th)
+	fun find []      n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
 	  | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
-			     then permute_prems n 1 0 th
+			     then permute_prems n 1 th
 			     else find ps (n+1)
     in
 	find (prems_of th) 0