# HG changeset patch
# User berghofe
# Date 1059602507 -7200
# Node ID c57ec95e7763439dd7d77265d0c04496d0a37407
# Parent  9b7a62788dac7d17f623b7d74e8dd636c2801b15
Removed extraneous rev in function goal_params (the list of parameters
is already reversed by rename_wrt_term).

diff -r 9b7a62788dac -r c57ec95e7763 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Jul 29 13:32:16 2003 +0200
+++ b/src/Pure/logic.ML	Thu Jul 31 00:01:47 2003 +0200
@@ -345,7 +345,7 @@
 (*reverses parameters for substitution*)
 fun goal_params st i =
   let val gi = get_goal st i
-      val rfrees = rev (map Free (rename_wrt_term gi (strip_params gi)))
+      val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   in (gi, rfrees) end;
 
 fun concl_of_goal st i =