# HG changeset patch
# User paulson
# Date 1181819804 -7200
# Node ID 925b381b4eea881ca0846ce8f291461fe22b056d
# Parent  5460951833fa35196d0f38200d4f7f95d96189d0
tidied

diff -r 5460951833fa -r 925b381b4eea src/Pure/tctical.ML
--- 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;