# HG changeset patch
# User nipkow
# Date 944560908 -3600
# Node ID 61eea7c23c5bc48b291f742cb390b411cf3bef98
# Parent  b7f7e18eb58494d8e61e8c57fbbbd71e21001593
Fixed bug in find-functions: list of parameters must be reversed before
subsitution.

diff -r b7f7e18eb584 -r 61eea7c23c5b src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Mon Dec 06 14:23:45 1999 +0100
+++ b/src/Pure/Thy/thm_database.ML	Tue Dec 07 11:01:48 1999 +0100
@@ -142,21 +142,21 @@
       val named_thms = thms_containing [c]
   in filter topc named_thms end;
 
-(*assume that parameters have unique names*)
+(*assume that parameters have unique names; reverse them for substitution*)
 fun goal_params i =
   let val gi = getgoal i
-      val frees = map Free (Logic.strip_params gi)
-  in (gi,frees) end;
+      val rfrees = rev(map Free (Logic.strip_params gi))
+  in (gi,rfrees) end;
 
 fun concl_of_goal i =
-  let val (gi,frees) = goal_params i
+  let val (gi,rfrees) = goal_params i
       val B = Logic.strip_assums_concl gi
-  in subst_bounds(frees,B) end;
+  in subst_bounds(rfrees,B) end;
 
 fun prems_of_goal i =
-  let val (gi,frees) = goal_params i
+  let val (gi,rfrees) = goal_params i
       val As = Logic.strip_assums_hyp gi
-  in map (fn A => subst_bounds(frees,A)) As end;
+  in map (fn A => subst_bounds(rfrees,A)) As end;
 
 (*returns all those named_thms whose subterm extracted by extract can be
   instantiated to obj; the list is sorted according to the number of premises