
diff -r 6e9e3cba4be9 -r f8a35cf814de QuotMain.thy
--- a/QuotMain.thy	Thu Oct 22 01:15:01 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 01:16:42 2009 +0200
@@ -1009,7 +1009,7 @@
   done
 
 ML {*
-fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, context, ...} =>
+fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
 let
   val pat = Drule.strip_imp_concl (cprop_of thm)
   val insts = Thm.match (pat, concl)




