Removed extraneous rev in function goal_params (the list of parameters
is already reversed by rename_wrt_term).
--- 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 =