author | Christian Urban <urbanc@in.tum.de> |
Thu, 22 Oct 2009 01:16:42 +0200 | |
changeset 147 | f8a35cf814de |
parent 146 | 6e9e3cba4be9 |
child 148 | 8e24e65f1e9b |
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)