src/Pure/Isar/local_defs.ML

--- a/src/Pure/Isar/local_defs.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -225,7 +225,7 @@
           ALLGOALS
             (CONVERSION (meta_rewrite_conv ctxt'') THEN'
               rewrite_goal_tac ctxt'' [def] THEN'
-              resolve_tac [Drule.reflexive_thm]))
+              resolve_tac ctxt'' [Drule.reflexive_thm]))
       handle ERROR msg => cat_error msg "Failed to prove definitional specification";
   in (((c, T), rhs), prove) end;