# HG changeset patch
# User wenzelm
# Date 1248804238 -7200
# Node ID eb97888fa422e11483071eb7b60cdb00a2101d27
# Parent  8b03a3daba5da3faed6fe405553468a8cd2f57f2
eliminated METAHYPS;

diff -r 8b03a3daba5d -r eb97888fa422 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Tue Jul 28 19:49:42 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML	Tue Jul 28 20:03:58 2009 +0200
@@ -67,8 +67,8 @@
         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
         imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
 
-(*val hyp_resolve_tac = METAHYPS (fn prems =>
-                                  resolve_tac (List.concat (map atomizeD prems)) 1);
+(*val hyp_resolve_tac = FOCUS (fn {prems, ...} =>
+                                  resolve_tac (maps atomizeD prems) 1);
   -- is nice, but cannot instantiate unknowns in the assumptions *)
 fun hyp_resolve_tac i st = let
         fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))