--- a/src/Pure/tctical.ML Fri Mar 10 00:53:28 2006 +0100
+++ b/src/Pure/tctical.ML Fri Mar 10 04:02:53 2006 +0100
@@ -482,7 +482,35 @@
in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end
handle TERM ("nth_prem", [A]) => NONE;
-fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf);
+
+fun find_vars thy (Const(c,tp)) vars =
+ let val tvars = Term.typ_tvars tp
+ in
+ case tvars of [] => vars
+ | _ => insert (op =) (c ^ " has type: " ^ (Sign.string_of_typ thy tp)) vars
+ end
+ | find_vars thy (t as Var(_,_)) vars =
+ insert (op =) ("Var " ^ (Term.str_of_term t)) vars
+ | find_vars _ (Free(_,_)) vars = vars
+ | find_vars _ (Bound _) vars = vars
+ | find_vars thy (Abs(_,tp,b)) vars = find_vars thy b vars
+ | find_vars thy (t1 $ t2) vars =
+ find_vars thy t2 (find_vars thy t1 vars);
+
+
+fun warning_multi [] = ()
+ | warning_multi (str1::strs) =
+ (warning str1; warning_multi strs);
+
+fun print_vars_terms thy (n,thm) =
+ let val prem = Logic.nth_prem (n, Thm.prop_of thm)
+ val tms = find_vars thy prem []
+ in
+ (warning "Found schematic vars in assumptions: "; warning_multi tms)
+ end;
+
+fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
+ handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty;