summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 14 Jun 2007 13:16:44 +0200 | |

changeset 23384 | 925b381b4eea |

parent 23383 | 5460951833fa |

child 23385 | 0ef4f9fc0d09 |

tidied

--- a/src/Pure/tctical.ML Thu Jun 14 10:38:48 2007 +0200 +++ b/src/Pure/tctical.ML Thu Jun 14 13:16:44 2007 +0200 @@ -480,8 +480,8 @@ (*Returns the theorem list that METAHYPS would supply to its tactic*) fun metahyps_thms i state = let val prem = Logic.nth_prem (i, Thm.prop_of state) - val (insts,params,hyps,concl) = metahyps_split_prem prem - val cterm = cterm_of (Thm.theory_of_thm state) + and cterm = cterm_of (Thm.theory_of_thm state) + val (_,_,hyps,_) = metahyps_split_prem prem in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end handle TERM ("nth_prem", [A]) => NONE;