more conventional tactic setup;
authorwenzelm
Tue Feb 14 21:45:32 2012 +0100 (2012-02-14)
changeset 46473a687b75f9fa8
parent 46472 06ca0a613687
child 46474 7e6be8270ddb
more conventional tactic setup;
src/HOL/Prolog/Test.thy
src/HOL/Prolog/prolog.ML
     1.1 --- a/src/HOL/Prolog/Test.thy	Tue Feb 14 21:31:26 2012 +0100
     1.2 +++ b/src/HOL/Prolog/Test.thy	Tue Feb 14 21:45:32 2012 +0100
     1.3 @@ -270,11 +270,5 @@
     1.4    apply (prolog prog_Test)
     1.5    back
     1.6    done
     1.7 -(*
     1.8 -back
     1.9 --> problem with DEPTH_SOLVE:
    1.10 -Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
    1.11 -Exception raised at run-time
    1.12 -*)
    1.13  
    1.14  end
     2.1 --- a/src/HOL/Prolog/prolog.ML	Tue Feb 14 21:31:26 2012 +0100
     2.2 +++ b/src/HOL/Prolog/prolog.ML	Tue Feb 14 21:45:32 2012 +0100
     2.3 @@ -71,7 +71,8 @@
     2.4  (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
     2.5                                    resolve_tac (maps atomizeD prems) 1);
     2.6    -- is nice, but cannot instantiate unknowns in the assumptions *)
     2.7 -fun hyp_resolve_tac i st = let
     2.8 +val hyp_resolve_tac = SUBGOAL (fn (subgoal, i) =>
     2.9 +  let
    2.10          fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    2.11          |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    2.12          |   ap t                          =                         (0,false,t);
    2.13 @@ -83,7 +84,6 @@
    2.14          val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
    2.15                                                  (#3(dest_state (st,i)));
    2.16  *)
    2.17 -        val subgoal = #3(Thm.dest_state (st,i));
    2.18          val prems = Logic.strip_assums_hyp subgoal;
    2.19          val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
    2.20          fun drot_tac k i = DETERM (rotate_tac k i);
    2.21 @@ -104,7 +104,7 @@
    2.22                  else no_tac);
    2.23          val ptacs = mapn (fn n => fn t =>
    2.24                            pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
    2.25 -        in Library.foldl (op APPEND) (no_tac, ptacs) st end;
    2.26 +  in Library.foldl (op APPEND) (no_tac, ptacs) end);
    2.27  
    2.28  fun ptac ctxt prog = let
    2.29    val proga = maps (atomizeD ctxt) prog         (* atomize the prog *)