# HG changeset patch
# User wenzelm
# Date 1027799714 -7200
# Node ID e0e2351043d239d61c4047d8171711a102a5aa53
# Parent  119ae829ad9b22aeb97072128f37a088c467437e
make SML/NJ happy;

diff -r 119ae829ad9b -r e0e2351043d2 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Jul 26 21:09:39 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jul 27 21:55:14 2002 +0200
@@ -1208,7 +1208,7 @@
       | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
   in
     if null (foldr Term.add_typ_tvars (map snd fixes, [])) andalso
-      null (foldr Term.add_term_vars (flat (map #2 assumes), [])) then
+      null (foldr Term.add_term_vars (flat (map snd assumes), [])) then
         {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds}
     else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
   end;