# HG changeset patch
# User wenzelm
# Date 1190581201 -7200
# Node ID 8113d01493047455e98b110c50d81fd6b636cf2f
# Parent  c3d56f41483bc1e70f9ee664cad2498e5515b685
made smlnj happy;

diff -r c3d56f41483b -r 8113d0149304 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Sep 23 22:23:37 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Sep 23 23:00:01 2007 +0200
@@ -766,8 +766,8 @@
         val binds = simult_matches ctxt2 (t, pats);
       in (binds, ctxt2) end;
 
-    val ts = prep_terms ctxt dummyT (map #2 raw_binds);
-    val (binds, ctxt') = apfst flat (fold_map prep_bind (map #1 raw_binds ~~ ts) ctxt);
+    val ts = prep_terms ctxt dummyT (map snd raw_binds);
+    val (binds, ctxt') = apfst flat (fold_map prep_bind (map fst raw_binds ~~ ts) ctxt);
     val binds' =
       if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds)
       else binds;