Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorChristian Urban <urbanc@in.tum.de>
Thu, 22 Oct 2009 01:16:42 +0200
changeset 147 f8a35cf814de
parent 146 6e9e3cba4be9
child 148 8e24e65f1e9b
tuned
QuotMain.thy file | annotate | diff | comparison | revisions 
--- 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)
nominal2