1.1 --- a/src/Pure/tctical.ML	Tue Feb 28 11:07:13 2006 +0100
     1.2 +++ b/src/Pure/tctical.ML	Tue Feb 28 11:07:54 2006 +0100
     1.3 @@ -34,6 +34,7 @@
     1.4    val INTLEAVE          : tactic * tactic -> tactic
     1.5    val INTLEAVE'         : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
     1.6    val METAHYPS          : (thm list -> tactic) -> int -> tactic
     1.7 +  val metahyps_thms     : int -> thm -> thm list option
     1.8    val no_tac            : tactic
     1.9    val ORELSE            : tactic * tactic -> tactic
    1.10    val ORELSE'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    1.11 @@ -410,19 +411,25 @@
    1.12    fun mk_inst (var as Var(v,T))  = (var,  free_of "METAHYP1_" (v,T))
    1.13  in
    1.14  
    1.15 -fun metahyps_aux_tac tacf (prem,i) state =
    1.16 -  let val {sign,maxidx,...} = rep_thm state
    1.17 -      val cterm = cterm_of sign
    1.18 -      (*find all vars in the hyps -- should find tvars also!*)
    1.19 +(*Common code for METAHYPS and metahyps_thms*)
    1.20 +fun metahyps_split_prem prem =
    1.21 +  let (*find all vars in the hyps -- should find tvars also!*)
    1.22        val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem)
    1.23        val insts = map mk_inst hyps_vars
    1.24        (*replace the hyps_vars by Frees*)
    1.25        val prem' = subst_atomic insts prem
    1.26        val (params,hyps,concl) = strip_context prem'
    1.27 +  in (insts,params,hyps,concl)  end;
    1.28 +
    1.29 +fun metahyps_aux_tac tacf (prem,gno) state =
    1.30 +  let val (insts,params,hyps,concl) = metahyps_split_prem prem 
    1.31 +      val {sign,maxidx,...} = rep_thm state
    1.32 +      val cterm = cterm_of sign
    1.33 +      val chyps = map cterm hyps
    1.34 +      val hypths = map assume chyps
    1.35 +      val subprems = map (forall_elim_vars 0) hypths
    1.36        val fparams = map Free params
    1.37        val cparams = map cterm fparams
    1.38 -      and chyps = map cterm hyps
    1.39 -      val hypths = map assume chyps
    1.40        fun swap_ctpair (t,u) = (cterm u, cterm t)
    1.41        (*Subgoal variables: make Free; lift type over params*)
    1.42        fun mk_subgoal_inst concl_vars (var as Var(v,T)) =
    1.43 @@ -460,14 +467,21 @@
    1.44                  (implies_intr_list emBs
    1.45                    (forall_intr_list cparams (implies_intr_list chyps Cth)))
    1.46          end
    1.47 -      val subprems = map (forall_elim_vars 0) hypths
    1.48 -      and st0 = trivial (cterm concl)
    1.49        (*function to replace the current subgoal*)
    1.50        fun next st = bicompose false (false, relift st, nprems_of st)
    1.51 -                    i state
    1.52 -  in Seq.maps next (tacf subprems st0) end;
    1.53 +                    gno state
    1.54 +  in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
    1.55 +
    1.56  end;
    1.57  
    1.58 +(*Returns the theorem list that METAHYPS would supply to its tactic*)
    1.59 +fun metahyps_thms i state =
    1.60 +  let val prem = Logic.nth_prem (i, Thm.prop_of state) 
    1.61 +      val (insts,params,hyps,concl) = metahyps_split_prem prem 
    1.62 +      val cterm = cterm_of (#sign (rep_thm state))
    1.63 +  in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end
    1.64 +  handle TERM ("nth_prem", [A]) => NONE;
    1.65 +
    1.66  fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf);
    1.67  
    1.68  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)