# HG changeset patch
# User wenzelm
# Date 1213631682 -7200
# Node ID f656a12e0f4efb16e22ff712782406be685dbff9
# Parent  4f7976a6ffc3d6130cb44dc67059661d18ac858a
ptac/prolog_tac: proper context;

diff -r 4f7976a6ffc3 -r f656a12e0f4e src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Mon Jun 16 17:54:39 2008 +0200
+++ b/src/HOL/Prolog/HOHH.thy	Mon Jun 16 17:54:42 2008 +0200
@@ -11,11 +11,11 @@
 begin
 
 method_setup ptac =
-  {* Method.thms_args (Method.SIMPLE_METHOD' o Prolog.ptac) *}
+  {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
   "Basic Lambda Prolog interpreter"
 
 method_setup prolog =
-  {* Method.thms_args (Method.SIMPLE_METHOD o Prolog.prolog_tac) *}
+  {* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
   "Lambda Prolog interpreter"
 
 consts
diff -r 4f7976a6ffc3 -r f656a12e0f4e src/HOL/Prolog/prolog.ML
--- a/src/HOL/Prolog/prolog.ML	Mon Jun 16 17:54:39 2008 +0200
+++ b/src/HOL/Prolog/prolog.ML	Mon Jun 16 17:54:42 2008 +0200
@@ -50,10 +50,10 @@
 fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
                         then thm else raise not_HOHH);
 
-fun atomizeD thm = let
+fun atomizeD ctxt thm = let
     fun at  thm = case concl_of thm of
-      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (Drule.read_instantiate [("x",
-                                        "?"^(if s="P" then "PP" else s))] spec))
+      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS
+        (RuleInsts.read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
     | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
     | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
     | _                             => [thm]
@@ -106,8 +106,8 @@
                           pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
         in Library.foldl (op APPEND) (no_tac, ptacs) st end;
 
-fun ptac prog = let
-  val proga = List.concat (map atomizeD prog)                   (* atomize the prog *)
+fun ptac ctxt prog = let
+  val proga = List.concat (map (atomizeD ctxt) prog)                   (* atomize the prog *)
   in    (REPEAT_DETERM1 o FIRST' [
                 rtac TrueI,                     (* "True" *)
                 rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
@@ -122,8 +122,9 @@
                  THEN' (fn _ => check_HOHH_tac2))
 end;
 
-fun prolog_tac prog = check_HOHH_tac1 THEN
-                      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
+fun prolog_tac ctxt prog =
+  check_HOHH_tac1 THEN
+  DEPTH_SOLVE (ptac ctxt (map check_HOHH prog) 1);
 
 val prog_HOHH = [];