--- 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