adapted to kernel changes
authorobua
Thu Feb 16 03:23:57 2006 +0100 (2006-02-16)
changeset 19066df24f2564aaa
parent 19065 82e2d66f995b
child 19067 c0321d7d6b3d
adapted to kernel changes
src/HOL/Import/proof_kernel.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Feb 16 00:09:46 2006 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Feb 16 03:23:57 2006 +0100
     1.3 @@ -1053,9 +1053,9 @@
     1.4  fun rearrange sg tm th =
     1.5      let
     1.6  	val tm' = Envir.beta_eta_contract tm
     1.7 -	fun find []      n = permute_prems 0 1 0 (implies_intr (Thm.cterm_of sg tm) th)
     1.8 +	fun find []      n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
     1.9  	  | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
    1.10 -			     then permute_prems n 1 0 th
    1.11 +			     then permute_prems n 1 th
    1.12  			     else find ps (n+1)
    1.13      in
    1.14  	find (prems_of th) 0