# HG changeset patch
# User wenzelm
# Date 1329252332 -3600
# Node ID a687b75f9fa871e58ed36759a289d7653cf35566
# Parent  06ca0a6136879a9774f3aab83c864d203293d028
more conventional tactic setup;

diff -r 06ca0a613687 -r a687b75f9fa8 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Tue Feb 14 21:31:26 2012 +0100
+++ b/src/HOL/Prolog/Test.thy	Tue Feb 14 21:45:32 2012 +0100
@@ -270,11 +270,5 @@
   apply (prolog prog_Test)
   back
   done
-(*
-back
--> problem with DEPTH_SOLVE:
-Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
-Exception raised at run-time
-*)
 
 end
diff -r 06ca0a613687 -r a687b75f9fa8 src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Tue Feb 14 21:31:26 2012 +0100
+++ b/src/HOL/Prolog/prolog.ML	Tue Feb 14 21:45:32 2012 +0100
@@ -71,7 +71,8 @@
 (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
                                   resolve_tac (maps atomizeD prems) 1);
   -- is nice, but cannot instantiate unknowns in the assumptions *)
-fun hyp_resolve_tac i st = let
+val hyp_resolve_tac = SUBGOAL (fn (subgoal, i) =>
+  let
         fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
         |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
         |   ap t                          =                         (0,false,t);
@@ -83,7 +84,6 @@
         val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
                                                 (#3(dest_state (st,i)));
 *)
-        val subgoal = #3(Thm.dest_state (st,i));
         val prems = Logic.strip_assums_hyp subgoal;
         val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
         fun drot_tac k i = DETERM (rotate_tac k i);
@@ -104,7 +104,7 @@
                 else no_tac);
         val ptacs = mapn (fn n => fn t =>
                           pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
-        in Library.foldl (op APPEND) (no_tac, ptacs) st end;
+  in Library.foldl (op APPEND) (no_tac, ptacs) end);
 
 fun ptac ctxt prog = let
   val proga = maps (atomizeD ctxt) prog         (* atomize the prog *)