# HG changeset patch
# User haftmann
# Date 1277363090 -7200
# Node ID 8a226fd561f8c1c920e1e593013978e8e5976b22
# Parent  9fc2ae73c5caaac219d284743f7a64585a9ea5be
made smlnj happy

diff -r 9fc2ae73c5ca -r 8a226fd561f8 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Jun 23 16:28:12 2010 +0200
+++ b/src/Pure/Isar/code.ML	Thu Jun 24 09:04:50 2010 +0200
@@ -1132,7 +1132,7 @@
     fun mk_prem z = Free (z, T_cong);
     fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
     val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
-    fun tac { prems, ... } = Simplifier.rewrite_goals_tac prems
+    fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
       THEN ALLGOALS (ProofContext.fact_tac [Drule.reflexive_thm]);
   in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end;