simplified oracle interface;
authorwenzelm
Thu Sep 18 19:39:44 2008 +0200 (2008-09-18 ago)
changeset 282904cc2b6046258
parent 28289 efd53393412b
child 28291 c49b328d689d
simplified oracle interface;
NEWS
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarRef/Thy/Spec.thy
src/FOL/ex/IffOracle.thy
src/HOL/ATP_Linkup.thy
src/HOL/Code_Setup.thy
src/HOL/Complex/ex/MIR.thy
src/HOL/Complex/ex/ReflectedFerrack.thy
src/HOL/Complex/ex/linrtac.ML
src/HOL/Complex/ex/mirtac.ML
src/HOL/Library/Eval_Witness.thy
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Presburger.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/res_atp_methods.ML
src/HOL/Tools/res_atp_provers.ML
src/HOL/ex/Reflected_Presburger.thy
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/coopertac.ML
src/HOL/ex/svc_funcs.ML
src/HOLCF/IOA/Modelcheck/MuIOA.thy
src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/skip_proof.ML
src/Pure/display.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Tools/Compute_Oracle/Compute_Oracle.thy
src/Tools/Compute_Oracle/compute.ML
src/Tools/nbe.ML
     1.1 --- a/NEWS	Thu Sep 18 14:06:58 2008 +0200
     1.2 +++ b/NEWS	Thu Sep 18 19:39:44 2008 +0200
     1.3 @@ -22,6 +22,13 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
     1.8 +to 'a -> thm, at the cost of internal tagging of results with an
     1.9 +authentic oracle name.  The Isar command 'oracle' is now polymorphic,
    1.10 +no argument type is specified.  INCOMPATIBILITY, need to simplify
    1.11 +existing oracle code accordingly.  Note that extra performance may be
    1.12 +gained by producing the cterm carefully, not via Thm.cterm_of.
    1.13 +
    1.14  * Changed defaults for unify configuration options:
    1.15  
    1.16    unify_trace_bound = 50 (formerly 25)
     2.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 18 14:06:58 2008 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 18 19:39:44 2008 +0200
     2.3 @@ -595,12 +595,12 @@
     2.4    @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
     2.5    @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
     2.6    @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
     2.7 -  @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
     2.8 +  @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
     2.9 +  -> (string * ('a -> thm)) * theory"} \\
    2.10    \end{mldecls}
    2.11    \begin{mldecls}
    2.12    @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
    2.13    @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
    2.14 -  @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
    2.15    @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
    2.16    \end{mldecls}
    2.17  
    2.18 @@ -651,16 +651,13 @@
    2.19    \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
    2.20    axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
    2.21  
    2.22 -  \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a
    2.23 -  named oracle function, cf.\ @{text "axiom"} in
    2.24 -  \figref{fig:prim-rules}.
    2.25 +  \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
    2.26 +  oracle rule, essentially generating arbitrary axioms on the fly,
    2.27 +  cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
    2.28  
    2.29    \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
    2.30    arbitrary propositions as axioms.
    2.31  
    2.32 -  \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle
    2.33 -  function for generating arbitrary axioms on the fly.
    2.34 -
    2.35    \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
    2.36    \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
    2.37    for constant @{text "c\<^isub>\<tau>"}, relative to existing
     3.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu Sep 18 14:06:58 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Sep 18 19:39:44 2008 +0200
     3.3 @@ -1136,9 +1136,8 @@
     3.4      @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
     3.5    \end{matharray}
     3.6  
     3.7 -  The oracle interface promotes a given ML function @{ML_text
     3.8 -  "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some
     3.9 -  type @{ML_text T} given by the user.  This acts like an infinitary
    3.10 +  The oracle interface promotes a given ML function @{ML_text "'a -> cterm"}
    3.11 +  to @{ML_text "'a -> thm"}.  This acts like an infinitary
    3.12    specification of axioms -- there is no internal check of the
    3.13    correctness of the results!  The inference kernel records oracle
    3.14    invocations within the internal derivation object of theorems, and
    3.15 @@ -1146,18 +1145,16 @@
    3.16    that are not fully checked by Isabelle inferences.
    3.17  
    3.18    \begin{rail}
    3.19 -    'oracle' name '(' type ')' '=' text
    3.20 +    'oracle' name '=' text
    3.21      ;
    3.22    \end{rail}
    3.23  
    3.24    \begin{descr}
    3.25  
    3.26 -  \item [@{command "oracle"}~@{text "name (type) = text"}] turns the
    3.27 -  given ML expression @{text "text"} of type
    3.28 -  @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an
    3.29 -  ML function of type
    3.30 -  @{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is
    3.31 -  bound to the global identifier @{ML_text name}.
    3.32 +  \item [@{command "oracle"}~@{text "name = text"}] turns the given ML
    3.33 +  expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
    3.34 +  ML function of type @{ML_text "'a -> thm"}, which is bound to the
    3.35 +  global identifier @{ML_text name}.
    3.36  
    3.37    \end{descr}
    3.38  *}
     4.1 --- a/src/FOL/ex/IffOracle.thy	Thu Sep 18 14:06:58 2008 +0200
     4.2 +++ b/src/FOL/ex/IffOracle.thy	Thu Sep 18 19:39:44 2008 +0200
     4.3 @@ -18,14 +18,14 @@
     4.4    and positive.
     4.5  *}
     4.6  
     4.7 -oracle iff_oracle (int) = {*
     4.8 +oracle iff_oracle = {*
     4.9    let
    4.10      fun mk_iff 1 = Var (("P", 0), @{typ o})
    4.11        | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
    4.12    in
    4.13 -    fn thy => fn n =>
    4.14 +    fn (thy, n) =>
    4.15        if n > 0 andalso n mod 2 = 0
    4.16 -      then FOLogic.mk_Trueprop (mk_iff n)
    4.17 +      then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n))
    4.18        else raise Fail ("iff_oracle: " ^ string_of_int n)
    4.19    end
    4.20  *}
    4.21 @@ -33,19 +33,19 @@
    4.22  
    4.23  subsection {* Oracle as low-level rule *}
    4.24  
    4.25 -ML {* iff_oracle @{theory} 2 *}
    4.26 -ML {* iff_oracle @{theory} 10 *}
    4.27 -ML {* #der (Thm.rep_thm (iff_oracle @{theory} 10)) *}
    4.28 +ML {* iff_oracle (@{theory}, 2) *}
    4.29 +ML {* iff_oracle (@{theory}, 10) *}
    4.30 +ML {* #der (Thm.rep_thm (iff_oracle (@{theory}, 10))) *}
    4.31  
    4.32  text {* These oracle calls had better fail. *}
    4.33  
    4.34  ML {*
    4.35 -  (iff_oracle @{theory} 5; error "?")
    4.36 +  (iff_oracle (@{theory}, 5); error "?")
    4.37      handle Fail _ => warning "Oracle failed, as expected"
    4.38  *}
    4.39  
    4.40  ML {*
    4.41 -  (iff_oracle @{theory} 1; error "?")
    4.42 +  (iff_oracle (@{theory}, 1); error "?")
    4.43      handle Fail _ => warning "Oracle failed, as expected"
    4.44  *}
    4.45  
    4.46 @@ -55,7 +55,7 @@
    4.47  method_setup iff = {*
    4.48    Method.simple_args OuterParse.nat (fn n => fn ctxt =>
    4.49      Method.SIMPLE_METHOD
    4.50 -      (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt) n))
    4.51 +      (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
    4.52          handle Fail _ => no_tac))
    4.53  *} "iff oracle"
    4.54  
     5.1 --- a/src/HOL/ATP_Linkup.thy	Thu Sep 18 14:06:58 2008 +0200
     5.2 +++ b/src/HOL/ATP_Linkup.thy	Thu Sep 18 19:39:44 2008 +0200
     5.3 @@ -101,9 +101,9 @@
     5.4  
     5.5  use "Tools/res_atp_provers.ML"
     5.6  
     5.7 -oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *}
     5.8 -oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *}
     5.9 -oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}
    5.10 +oracle vampire_oracle = {* ResAtpProvers.vampire_o *}
    5.11 +oracle eprover_oracle = {* ResAtpProvers.eprover_o *}
    5.12 +oracle spass_oracle = {* ResAtpProvers.spass_o *}
    5.13  
    5.14  use "Tools/res_atp_methods.ML"
    5.15  setup ResAtpMethods.setup      --{*Oracle ATP methods: still useful?*}
     6.1 --- a/src/HOL/Code_Setup.thy	Thu Sep 18 14:06:58 2008 +0200
     6.2 +++ b/src/HOL/Code_Setup.thy	Thu Sep 18 19:39:44 2008 +0200
     6.3 @@ -129,17 +129,22 @@
     6.4  end;
     6.5  *}
     6.6  
     6.7 -oracle eval_oracle ("term") = {* fn thy => fn t => 
     6.8 -  if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
     6.9 -    (HOLogic.dest_Trueprop t) [] 
    6.10 -  then t
    6.11 -  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    6.12 +oracle eval_oracle = {* fn ct =>
    6.13 +  let
    6.14 +    val thy = Thm.theory_of_cterm ct;
    6.15 +    val t = Thm.term_of ct;
    6.16 +  in
    6.17 +    if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
    6.18 +      (HOLogic.dest_Trueprop t) [] 
    6.19 +    then ct
    6.20 +    else @{cprop True} (*dummy*)
    6.21 +  end
    6.22  *}
    6.23  
    6.24  method_setup eval = {*
    6.25  let
    6.26    fun eval_tac thy = 
    6.27 -    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
    6.28 +    CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
    6.29  in 
    6.30    Method.ctxt_args (fn ctxt => 
    6.31      Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
     7.1 --- a/src/HOL/Complex/ex/MIR.thy	Thu Sep 18 14:06:58 2008 +0200
     7.2 +++ b/src/HOL/Complex/ex/MIR.thy	Thu Sep 18 19:39:44 2008 +0200
     7.3 @@ -5791,7 +5791,7 @@
     7.4  (*export_code mircfrqe mirlfrqe
     7.5    in SML module_name Mir file "raw_mir.ML"*)
     7.6  
     7.7 -oracle mirfr_oracle ("bool * term") = {*
     7.8 +oracle mirfr_oracle = {* fn (proofs, ct) =>
     7.9  let
    7.10  
    7.11  fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
    7.12 @@ -5891,13 +5891,15 @@
    7.13    | term_of_fm vs (@{code Iff} (t1, t2)) =
    7.14        @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ term_of_fm vs t1 $ term_of_fm vs t2;
    7.15  
    7.16 -in fn thy => fn (proofs, t) =>
    7.17 +in
    7.18    let 
    7.19 +    val thy = Thm.theory_of_cterm ct;
    7.20 +    val t = Thm.term_of ct;
    7.21      val fs = term_frees t;
    7.22      val vs = fs ~~ (0 upto (length fs - 1));
    7.23      val qe = if proofs then @{code mirlfrqe} else @{code mircfrqe};
    7.24      val t' = (term_of_fm vs o qe o fm_of_term vs) t;
    7.25 -  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
    7.26 +  in (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
    7.27  end;
    7.28  *}
    7.29  
     8.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Sep 18 14:06:58 2008 +0200
     8.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Sep 18 19:39:44 2008 +0200
     8.3 @@ -1997,7 +1997,7 @@
     8.4  
     8.5  ML {* @{code ferrack_test} () *}
     8.6  
     8.7 -oracle linr_oracle ("term") = {*
     8.8 +oracle linr_oracle = {*
     8.9  let
    8.10  
    8.11  fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
    8.12 @@ -2066,11 +2066,14 @@
    8.13        term_of_fm vs t1 $ term_of_fm vs t2
    8.14    | term_of_fm vs _ = error "If this is raised, Isabelle/HOL or generate_code is inconsistent.";
    8.15  
    8.16 -in fn thy => fn t =>
    8.17 +in fn ct =>
    8.18    let 
    8.19 +    val thy = Thm.theory_of_cterm ct;
    8.20 +    val t = Thm.term_of ct;
    8.21      val fs = term_frees t;
    8.22      val vs = fs ~~ (0 upto (length fs - 1));
    8.23 -  in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t)))) end
    8.24 +    val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, term_of_fm vs (@{code linrqe} (fm_of_term vs t))));
    8.25 +  in Thm.cterm_of thy res end
    8.26  end;
    8.27  *}
    8.28  
     9.1 --- a/src/HOL/Complex/ex/linrtac.ML	Thu Sep 18 14:06:58 2008 +0200
     9.2 +++ b/src/HOL/Complex/ex/linrtac.ML	Thu Sep 18 19:39:44 2008 +0200
     9.3 @@ -86,7 +86,7 @@
     9.4      (* The result of the quantifier elimination *)
     9.5      val (th, tac) = case (prop_of pre_thm) of
     9.6          Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
     9.7 -    let val pth = linr_oracle thy (Pattern.eta_long [] t1)
     9.8 +    let val pth = linr_oracle (cterm_of thy (Pattern.eta_long [] t1))
     9.9      in 
    9.10            (trace_msg ("calling procedure with term:\n" ^
    9.11               Syntax.string_of_term ctxt t1);
    10.1 --- a/src/HOL/Complex/ex/mirtac.ML	Thu Sep 18 14:06:58 2008 +0200
    10.2 +++ b/src/HOL/Complex/ex/mirtac.ML	Thu Sep 18 19:39:44 2008 +0200
    10.3 @@ -87,9 +87,9 @@
    10.4  
    10.5  fun mir_tac ctxt q i = 
    10.6      (ObjectLogic.atomize_prems_tac i)
    10.7 -	THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
    10.8 -	THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
    10.9 -	THEN (fn st =>
   10.10 +        THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
   10.11 +        THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
   10.12 +        THEN (fn st =>
   10.13    let
   10.14      val g = List.nth (prems_of st, i - 1)
   10.15      val thy = ProofContext.theory_of ctxt
   10.16 @@ -97,13 +97,13 @@
   10.17      val (t,np,nh) = prepare_for_mir thy q g
   10.18      (* Some simpsets for dealing with mod div abs and nat*)
   10.19      val mod_div_simpset = HOL_basic_ss 
   10.20 -			addsimps [refl,nat_mod_add_eq, 
   10.21 -				  @{thm "mod_self"}, @{thm "zmod_self"},
   10.22 -				  @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
   10.23 -				  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
   10.24 -				  @{thm "Suc_plus1"}]
   10.25 -			addsimps @{thms add_ac}
   10.26 -			addsimprocs [cancel_div_mod_proc]
   10.27 +                        addsimps [refl,nat_mod_add_eq, 
   10.28 +                                  @{thm "mod_self"}, @{thm "zmod_self"},
   10.29 +                                  @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
   10.30 +                                  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
   10.31 +                                  @{thm "Suc_plus1"}]
   10.32 +                        addsimps @{thms add_ac}
   10.33 +                        addsimprocs [cancel_div_mod_proc]
   10.34      val simpset0 = HOL_basic_ss
   10.35        addsimps [mod_div_equality', Suc_plus1]
   10.36        addsimps comp_ths
   10.37 @@ -131,11 +131,11 @@
   10.38      (* The result of the quantifier elimination *)
   10.39      val (th, tac) = case (prop_of pre_thm) of
   10.40          Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
   10.41 -    let val pth = 
   10.42 +    let val pth =
   10.43            (* If quick_and_dirty then run without proof generation as oracle*)
   10.44 -             if !quick_and_dirty 
   10.45 -             then mirfr_oracle thy (false, Pattern.eta_long [] t1)
   10.46 -	     else mirfr_oracle thy (true, Pattern.eta_long [] t1)
   10.47 +             if !quick_and_dirty
   10.48 +             then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
   10.49 +             else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
   10.50      in 
   10.51            (trace_msg ("calling procedure with term:\n" ^
   10.52               Syntax.string_of_term ctxt t1);
    11.1 --- a/src/HOL/Library/Eval_Witness.thy	Thu Sep 18 14:06:58 2008 +0200
    11.2 +++ b/src/HOL/Library/Eval_Witness.thy	Thu Sep 18 19:39:44 2008 +0200
    11.3 @@ -55,8 +55,10 @@
    11.4  end;
    11.5  *}
    11.6  
    11.7 -oracle eval_witness_oracle ("term * string list") = {* fn thy => fn (goal, ws) => 
    11.8 +oracle eval_witness_oracle = {* fn (cgoal, ws) =>
    11.9  let
   11.10 +  val thy = Thm.theory_of_cterm cgoal;
   11.11 +  val goal = Thm.term_of cgoal;
   11.12    fun check_type T = 
   11.13      if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
   11.14      then T
   11.15 @@ -69,8 +71,8 @@
   11.16    val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
   11.17  in
   11.18    if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
   11.19 -  then goal
   11.20 -  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
   11.21 +  then Thm.cterm_of thy goal
   11.22 +  else @{cprop True} (*dummy*)
   11.23  end
   11.24  *}
   11.25  
   11.26 @@ -78,12 +80,11 @@
   11.27  method_setup eval_witness = {*
   11.28  let
   11.29  
   11.30 -fun eval_tac ws thy = 
   11.31 -  SUBGOAL (fn (t, i) => rtac (eval_witness_oracle thy (t, ws)) i)
   11.32 +fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
   11.33  
   11.34 -in 
   11.35 -  Method.simple_args (Scan.repeat Args.name) (fn ws => fn ctxt => 
   11.36 -    Method.SIMPLE_METHOD' (eval_tac ws (ProofContext.theory_of ctxt)))
   11.37 +in
   11.38 +  Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
   11.39 +    Method.SIMPLE_METHOD' (eval_tac ws))
   11.40  end
   11.41  *} "Evaluation with ML witnesses"
   11.42  
    12.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Sep 18 14:06:58 2008 +0200
    12.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu Sep 18 19:39:44 2008 +0200
    12.3 @@ -30,7 +30,7 @@
    12.4    val trace_eindhoven = ref false;
    12.5  *}
    12.6  
    12.7 -oracle mc_eindhoven_oracle ("term") =
    12.8 +oracle mc_eindhoven_oracle =
    12.9  {*
   12.10  let
   12.11    val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
   12.12 @@ -43,15 +43,17 @@
   12.13          else eindhoven_home ^ "/pmu";
   12.14      in #1 (system_out ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w")) end;
   12.15  in
   12.16 -  fn thy => fn goal =>
   12.17 +  fn cgoal =>
   12.18      let
   12.19 +      val thy = Thm.theory_of_cterm cgoal;
   12.20 +      val goal = Thm.term_of cgoal;
   12.21        val s = eindhoven_term thy goal;
   12.22        val debug = tracing ("MC debugger: " ^ s);
   12.23        val result = call_mc s;
   12.24      in
   12.25        if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else ();
   12.26        (case result of
   12.27 -        "TRUE\n"  => goal |
   12.28 +        "TRUE\n"  => cgoal |
   12.29          "FALSE\n" => error "MC oracle yields FALSE" |
   12.30        _ => error ("MC syntax error: " ^ result))
   12.31      end
   12.32 @@ -62,7 +64,7 @@
   12.33  fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
   12.34    let
   12.35      val thy = Thm.theory_of_thm state;
   12.36 -    val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
   12.37 +    val assertion = mc_eindhoven_oracle (Thm.cterm_of thy (Logic.strip_imp_concl goal));
   12.38    in cut_facts_tac [assertion] i THEN atac i end) i state;
   12.39  
   12.40  val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
    13.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Thu Sep 18 14:06:58 2008 +0200
    13.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Thu Sep 18 19:39:44 2008 +0200
    13.3 @@ -68,8 +68,7 @@
    13.4    will be replaced by the expression between the two asterisks
    13.5    following "case" and the asterisk after esac will be deleted *)
    13.6  
    13.7 -oracle mc_mucke_oracle ("term") =
    13.8 -  mk_mc_mucke_oracle
    13.9 +oracle mc_mucke_oracle = mk_mc_mucke_oracle
   13.10  
   13.11  ML {*
   13.12  (* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
   13.13 @@ -154,12 +153,9 @@
   13.14  end;
   13.15  
   13.16  
   13.17 -fun call_mucke_tac i state =
   13.18 -let val thy = Thm.theory_of_thm state;
   13.19 -    val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
   13.20 -in 
   13.21 -(cut_facts_tac [OraAss] i) state
   13.22 -end;
   13.23 +val call_mucke_tac = CSUBGOAL (fn (cgoal, i) =>
   13.24 +let val OraAss = mc_mucke_oracle cgoal
   13.25 +in cut_facts_tac [OraAss] i end);
   13.26  
   13.27  
   13.28  (* transforming fun-defs into lambda-defs *)
    14.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu Sep 18 14:06:58 2008 +0200
    14.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu Sep 18 19:39:44 2008 +0200
    14.3 @@ -1012,8 +1012,12 @@
    14.4  
    14.5  (**********************************************************)
    14.6  
    14.7 -fun mk_mc_mucke_oracle sign subgoal = 
    14.8 -  let 	val Freesubgoal = freeze_thaw subgoal;
    14.9 +fun mk_mc_mucke_oracle csubgoal =
   14.10 +  let
   14.11 +  val sign = Thm.theory_of_cterm csubgoal;
   14.12 +  val subgoal = Thm.term_of csubgoal;
   14.13 +
   14.14 +	val Freesubgoal = freeze_thaw subgoal;
   14.15  
   14.16  	val prems = Logic.strip_imp_prems Freesubgoal; 
   14.17  	val concl = Logic.strip_imp_concl Freesubgoal; 
   14.18 @@ -1047,6 +1051,6 @@
   14.19  	(writeln ("\nmodelchecker input:\n" ^ MCstr ^ "\n/**** end ****/"))
   14.20            else ();
   14.21  (case (extract_result concl_str result) of 
   14.22 -	true  =>  (Logic.strip_imp_concl subgoal) | 
   14.23 +	true  =>  cterm_of sign (Logic.strip_imp_concl subgoal) | 
   14.24  	false => (error ("Mucke couldn't solve subgoal: \n" ^result)))) 
   14.25    end;
    15.1 --- a/src/HOL/Presburger.thy	Thu Sep 18 14:06:58 2008 +0200
    15.2 +++ b/src/HOL/Presburger.thy	Thu Sep 18 19:39:44 2008 +0200
    15.3 @@ -440,7 +440,7 @@
    15.4  by simp_all
    15.5  
    15.6  use "Tools/Qelim/cooper.ML"
    15.7 -oracle linzqe_oracle ("term") = Coopereif.cooper_oracle
    15.8 +oracle linzqe_oracle = Coopereif.cooper_oracle
    15.9  
   15.10  use "Tools/Qelim/presburger.ML"
   15.11  
    16.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Sep 18 14:06:58 2008 +0200
    16.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Sep 18 19:39:44 2008 +0200
    16.3 @@ -633,12 +633,14 @@
    16.4   | NClosed n => term_of_qf ps vs (Nota (Closed n))
    16.5   | _ => cooper "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
    16.6  
    16.7 -fun cooper_oracle thy t = 
    16.8 +fun cooper_oracle ct =
    16.9    let
   16.10 +    val thy = Thm.theory_of_cterm ct;
   16.11 +    val t = Thm.term_of ct;
   16.12      val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
   16.13    in
   16.14 -    Logic.mk_equals (HOLogic.mk_Trueprop t,
   16.15 -      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
   16.16 +    Thm.cterm_of thy (Logic.mk_equals (HOLogic.mk_Trueprop t,
   16.17 +      HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))))
   16.18    end;
   16.19  
   16.20  end;
    17.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Thu Sep 18 14:06:58 2008 +0200
    17.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Sep 18 19:39:44 2008 +0200
    17.3 @@ -152,8 +152,8 @@
    17.4     let 
    17.5      val cpth = 
    17.6         if !quick_and_dirty 
    17.7 -       then linzqe_oracle (ProofContext.theory_of ctxt) 
    17.8 -             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
    17.9 +       then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
   17.10 +             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
   17.11         else arg_conv (Cooper.cooper_conv ctxt) p
   17.12      val p' = Thm.rhs_of cpth
   17.13      val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
    18.1 --- a/src/HOL/Tools/res_atp_methods.ML	Thu Sep 18 14:06:58 2008 +0200
    18.2 +++ b/src/HOL/Tools/res_atp_methods.ML	Thu Sep 18 19:39:44 2008 +0200
    18.3 @@ -27,7 +27,7 @@
    18.4      Meson.skolemize_tac,
    18.5      METAHYPS (fn negs =>
    18.6        HEADGOAL (Tactic.rtac
    18.7 -        (res_atp_oracle (ProofContext.theory_of ctxt)
    18.8 +        (res_atp_oracle
    18.9            (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty;
   18.10  
   18.11  
    19.1 --- a/src/HOL/Tools/res_atp_provers.ML	Thu Sep 18 14:06:58 2008 +0200
    19.2 +++ b/src/HOL/Tools/res_atp_provers.ML	Thu Sep 18 19:39:44 2008 +0200
    19.3 @@ -40,19 +40,19 @@
    19.4    in seek_line "SPASS beiseite: Proof found.\n" instr
    19.5    end;
    19.6  
    19.7 -fun vampire_o _ (file,time) =
    19.8 +fun vampire_o (file,time) =
    19.9    if call_vampire (file,time)
   19.10 -  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
   19.11 +  then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
   19.12    else (ResAtp.cond_rm_tmp file; raise Fail ("vampire oracle failed"));
   19.13  
   19.14 -fun eprover_o _ (file,time) =
   19.15 +fun eprover_o (file,time) =
   19.16    if call_eprover (file,time)
   19.17 -  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
   19.18 +  then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
   19.19    else (ResAtp.cond_rm_tmp file; raise Fail ("eprover oracle failed"));
   19.20  
   19.21 -fun spass_o _ (file,time) =
   19.22 +fun spass_o (file,time) =
   19.23    if call_spass (file,time)
   19.24 -  then (warning file; ResAtp.cond_rm_tmp file; HOLogic.mk_Trueprop HOLogic.false_const)
   19.25 +  then (warning file; ResAtp.cond_rm_tmp file; @{cprop False})
   19.26    else (ResAtp.cond_rm_tmp file; raise Fail ("SPASS oracle failed"));
   19.27  
   19.28  end;
    20.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Thu Sep 18 14:06:58 2008 +0200
    20.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Thu Sep 18 19:39:44 2008 +0200
    20.3 @@ -1920,7 +1920,7 @@
    20.4  export_code pa in SML module_name GeneratedCooper file "~~/src/HOL/Tools/Qelim/raw_generated_cooper.ML"
    20.5  *)
    20.6  
    20.7 -oracle linzqe_oracle ("term") = {*
    20.8 +oracle linzqe_oracle = {*
    20.9  let
   20.10  
   20.11  fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
   20.12 @@ -2035,14 +2035,16 @@
   20.13      | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
   20.14    end;
   20.15  
   20.16 -in fn thy => fn t =>
   20.17 -  let 
   20.18 +in fn ct =>
   20.19 +  let
   20.20 +    val thy = Thm.theory_of_cterm ct;
   20.21 +    val t = Thm.term_of ct;
   20.22      val fs = term_frees t;
   20.23      val bs = term_bools [] t;
   20.24      val vs = fs ~~ (0 upto (length fs - 1))
   20.25      val ps = bs ~~ (0 upto (length bs - 1))
   20.26      val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
   20.27 -  in (HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
   20.28 +  in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
   20.29  end;
   20.30  *}
   20.31  
    21.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Sep 18 14:06:58 2008 +0200
    21.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Sep 18 19:39:44 2008 +0200
    21.3 @@ -19,8 +19,7 @@
    21.4  
    21.5  hide const iff_keep iff_unfold
    21.6  
    21.7 -oracle
    21.8 -  svc_oracle ("term") = Svc.oracle
    21.9 +oracle svc_oracle = Svc.oracle
   21.10  
   21.11  ML {*
   21.12  (*
   21.13 @@ -110,12 +109,13 @@
   21.14    abstracted.  Use via compose_tac, which performs no lifting but will
   21.15    instantiate variables.*)
   21.16  
   21.17 -fun svc_tac i st =
   21.18 +val svc_tac = CSUBGOAL (fn (ct, i) =>
   21.19    let
   21.20 -    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
   21.21 -    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
   21.22 -   in compose_tac (false, th, 0) i st end
   21.23 -   handle TERM _ => no_tac st;
   21.24 +    val thy = Thm.theory_of_cterm ct;
   21.25 +    val (abs_goal, _) = svc_abstract (Thm.term_of ct);
   21.26 +    val th = svc_oracle (Thm.cterm_of thy abs_goal);
   21.27 +   in compose_tac (false, th, 0) i end
   21.28 +   handle TERM _ => no_tac);
   21.29  *}
   21.30  
   21.31  end
    22.1 --- a/src/HOL/ex/coopertac.ML	Thu Sep 18 14:06:58 2008 +0200
    22.2 +++ b/src/HOL/ex/coopertac.ML	Thu Sep 18 19:39:44 2008 +0200
    22.3 @@ -104,7 +104,7 @@
    22.4      (* The result of the quantifier elimination *)
    22.5      val (th, tac) = case (prop_of pre_thm) of
    22.6          Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
    22.7 -    let val pth = linzqe_oracle thy (Pattern.eta_long [] t1)
    22.8 +    let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
    22.9      in 
   22.10            ((pth RS iffD2) RS pre_thm,
   22.11              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
    23.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Sep 18 14:06:58 2008 +0200
    23.2 +++ b/src/HOL/ex/svc_funcs.ML	Thu Sep 18 19:39:44 2008 +0200
    23.3 @@ -237,10 +237,14 @@
    23.4    end;
    23.5  
    23.6  
    23.7 - (*The oracle proves the given formula t, if possible*)
    23.8 - fun oracle thy t =
    23.9 -  (if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
   23.10 -   else ();
   23.11 -   if valid (expr_of false t) then t else fail t);
   23.12 + (*The oracle proves the given formula, if possible*)
   23.13 +  fun oracle ct =
   23.14 +    let
   23.15 +      val thy = Thm.theory_of_cterm ct;
   23.16 +      val t = Thm.term_of ct;
   23.17 +      val _ =
   23.18 +        if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
   23.19 +       else ();
   23.20 +    in if valid (expr_of false t) then ct else fail t end;
   23.21  
   23.22  end;
    24.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Sep 18 14:06:58 2008 +0200
    24.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Sep 18 19:39:44 2008 +0200
    24.3 @@ -178,8 +178,12 @@
    24.4  
    24.5  in
    24.6  
    24.7 -fun mk_sim_oracle sign (subgoal, thl) = (
    24.8 +fun mk_sim_oracle (csubgoal, thl) =
    24.9    let
   24.10 +    val sign = Thm.theory_of_cterm csubgoal;
   24.11 +    val subgoal = Thm.term_of csubgoal;
   24.12 +  in
   24.13 + (let
   24.14      val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
   24.15      val concl = Logic.strip_imp_concl subgoal;
   24.16      val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
   24.17 @@ -287,11 +291,12 @@
   24.18  by (atac 1);
   24.19  result();
   24.20  OldGoals.pop_proof();
   24.21 -Logic.strip_imp_concl subgoal
   24.22 +Thm.cterm_of sign (Logic.strip_imp_concl subgoal)
   24.23  )
   24.24  end)
   24.25  handle malformed =>
   24.26 -error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal));
   24.27 +error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal))
   24.28 +end;
   24.29  
   24.30  end
   24.31  
    25.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Sep 18 14:06:58 2008 +0200
    25.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy	Thu Sep 18 19:39:44 2008 +0200
    25.3 @@ -5,16 +5,13 @@
    25.4  imports MuIOA
    25.5  begin
    25.6  
    25.7 -oracle sim_oracle ("term * thm list") =
    25.8 -  mk_sim_oracle
    25.9 +oracle sim_oracle = mk_sim_oracle
   25.10  
   25.11  ML {*
   25.12  (* call_sim_tac invokes oracle "Sim" *)
   25.13 -fun call_sim_tac thm_list i state = 
   25.14 -let val thy = Thm.theory_of_thm state;
   25.15 -        val (subgoal::_) = Library.drop(i-1,prems_of state);
   25.16 -        val OraAss = sim_oracle thy (subgoal,thm_list);
   25.17 -in cut_facts_tac [OraAss] i state end;
   25.18 +fun call_sim_tac thm_list = CSUBGOAL (fn (csubgoal, i) =>
   25.19 +let val OraAss = sim_oracle (csubgoal,thm_list);
   25.20 +in cut_facts_tac [OraAss] i end);
   25.21  
   25.22  
   25.23  val ioa_implements_def = thm "ioa_implements_def";
    26.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Sep 18 14:06:58 2008 +0200
    26.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Sep 18 19:39:44 2008 +0200
    26.3 @@ -13,8 +13,7 @@
    26.4    val print_translation: bool * (string * Position.T) -> theory -> theory
    26.5    val typed_print_translation: bool * (string * Position.T) -> theory -> theory
    26.6    val print_ast_translation: bool * (string * Position.T) -> theory -> theory
    26.7 -  val oracle: bstring -> SymbolPos.text * Position.T -> SymbolPos.text * Position.T ->
    26.8 -    theory -> theory
    26.9 +  val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
   26.10    val add_axioms: ((Name.binding * string) * Attrib.src list) list -> theory -> theory
   26.11    val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory
   26.12    val declaration: string * Position.T -> local_theory -> local_theory
   26.13 @@ -152,22 +151,15 @@
   26.14  
   26.15  (* oracles *)
   26.16  
   26.17 -fun oracle name typ_pos (oracle_txt, pos) =
   26.18 +fun oracle name (oracle_txt, pos) =
   26.19    let
   26.20 -    val typ = SymbolPos.content (SymbolPos.explode typ_pos);
   26.21      val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
   26.22      val txt =
   26.23 -      "local\
   26.24 -      \  type T = " ^ typ ^ ";\
   26.25 -      \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
   26.26 +      "local\n\
   26.27        \  val name = " ^ quote name ^ ";\n\
   26.28 -      \  exception Arg of T;\n\
   26.29 -      \  val _ = Context.>> (Context.map_theory\n\
   26.30 -      \    (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
   26.31 -      \  val thy = ML_Context.the_global_context ();\n\
   26.32 -      \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
   26.33 +      \  val oracle = " ^ oracle ^ ";\n\
   26.34        \in\n\
   26.35 -      \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
   26.36 +      \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (name, oracle))));\n\
   26.37        \end;\n";
   26.38    in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
   26.39  
    27.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Sep 18 14:06:58 2008 +0200
    27.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Sep 18 19:39:44 2008 +0200
    27.3 @@ -371,8 +371,7 @@
    27.4  
    27.5  val _ =
    27.6    OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
    27.7 -    (P.name -- (P.$$$ "(" |-- P.ML_source --| P.$$$ ")" --| P.$$$ "=")
    27.8 -      -- P.ML_source >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
    27.9 +    (P.name -- (P.$$$ "=" |-- P.ML_source) >> (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
   27.10  
   27.11  
   27.12  (* local theories *)
    28.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Sep 18 14:06:58 2008 +0200
    28.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Sep 18 19:39:44 2008 +0200
    28.3 @@ -20,20 +20,15 @@
    28.4  
    28.5  (* oracle setup *)
    28.6  
    28.7 -exception SkipProof of term;
    28.8 -
    28.9 -fun skip_proof (_, SkipProof prop) =
   28.10 -  if ! quick_and_dirty then prop
   28.11 -  else error "Proof may be skipped in quick_and_dirty mode only!";
   28.12 -
   28.13 -val _ = Context.>> (Context.map_theory
   28.14 -  (Theory.add_oracle ("skip_proof", skip_proof)));
   28.15 +val (_, skip_proof) = Context.>>> (Context.map_theory_result
   28.16 +  (Thm.add_oracle ("skip_proof", fn (thy, prop) =>
   28.17 +    if ! quick_and_dirty then Thm.cterm_of thy prop
   28.18 +    else error "Proof may be skipped in quick_and_dirty mode only!")));
   28.19  
   28.20  
   28.21  (* basic cheating *)
   28.22  
   28.23 -fun make_thm thy prop =
   28.24 -  Thm.invoke_oracle_i thy "Pure.skip_proof" (thy, SkipProof prop);
   28.25 +fun make_thm thy prop = skip_proof (thy, prop);
   28.26  
   28.27  fun cheat_tac thy st =
   28.28    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    29.1 --- a/src/Pure/display.ML	Thu Sep 18 14:06:58 2008 +0200
    29.2 +++ b/src/Pure/display.ML	Thu Sep 18 19:39:44 2008 +0200
    29.3 @@ -178,7 +178,6 @@
    29.4        Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
    29.5  
    29.6      val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
    29.7 -    val oracles = (Theory.oracle_space thy, Theory.oracle_table thy);
    29.8      val defs = Theory.defs_of thy;
    29.9      val {restricts, reducts} = Defs.dest defs;
   29.10      val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
   29.11 @@ -202,7 +201,6 @@
   29.12      val cnstrs = NameSpace.extern_table constraints;
   29.13  
   29.14      val axms = NameSpace.extern_table axioms;
   29.15 -    val oras = NameSpace.extern_table oracles;
   29.16  
   29.17      val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
   29.18        |> map (fn (lhs, rhs) =>
   29.19 @@ -223,7 +221,7 @@
   29.20        Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
   29.21        Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
   29.22        Pretty.big_list "axioms:" (map pretty_axm axms),
   29.23 -      Pretty.strs ("oracles:" :: (map #1 oras)),
   29.24 +      Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
   29.25        Pretty.big_list "definitions:"
   29.26          [pretty_finals reds0,
   29.27           Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
    30.1 --- a/src/Pure/theory.ML	Thu Sep 18 14:06:58 2008 +0200
    30.2 +++ b/src/Pure/theory.ML	Thu Sep 18 19:39:44 2008 +0200
    30.3 @@ -2,7 +2,7 @@
    30.4      ID:         $Id$
    30.5      Author:     Lawrence C Paulson and Markus Wenzel
    30.6  
    30.7 -Logical theory content: axioms, definitions, oracles.
    30.8 +Logical theory content: axioms, definitions, and begin/end wrappers.
    30.9  *)
   30.10  
   30.11  signature THEORY =
   30.12 @@ -22,8 +22,6 @@
   30.13    val requires: theory -> string -> string -> unit
   30.14    val axiom_space: theory -> NameSpace.T
   30.15    val axiom_table: theory -> term Symtab.table
   30.16 -  val oracle_space: theory -> NameSpace.T
   30.17 -  val oracle_table: theory -> ((theory * Object.T -> term) * stamp) Symtab.table
   30.18    val axioms_of: theory -> (string * term) list
   30.19    val all_axioms_of: theory -> (string * term) list
   30.20    val defs_of: theory -> Defs.T
   30.21 @@ -39,7 +37,6 @@
   30.22    val add_finals: bool -> string list -> theory -> theory
   30.23    val add_finals_i: bool -> term list -> theory -> theory
   30.24    val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
   30.25 -  val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
   30.26  end
   30.27  
   30.28  structure Theory: THEORY =
   30.29 @@ -86,55 +83,41 @@
   30.30  datatype thy = Thy of
   30.31   {axioms: term NameSpace.table,
   30.32    defs: Defs.T,
   30.33 -  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
   30.34    wrappers: wrapper list * wrapper list};
   30.35  
   30.36 -fun make_thy (axioms, defs, oracles, wrappers) =
   30.37 -  Thy {axioms = axioms, defs = defs, oracles = oracles, wrappers = wrappers};
   30.38 +fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
   30.39  
   30.40  fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
   30.41 -fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
   30.42  
   30.43  structure ThyData = TheoryDataFun
   30.44  (
   30.45    type T = thy;
   30.46 -  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, ([], []));
   30.47 +  val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
   30.48    val copy = I;
   30.49  
   30.50 -  fun extend (Thy {axioms, defs, oracles, wrappers}) =
   30.51 -    make_thy (NameSpace.empty_table, defs, oracles, wrappers);
   30.52 +  fun extend (Thy {axioms, defs, wrappers}) = make_thy (NameSpace.empty_table, defs, wrappers);
   30.53  
   30.54    fun merge pp (thy1, thy2) =
   30.55      let
   30.56 -      val Thy {axioms = _, defs = defs1, oracles = oracles1, wrappers = (bgs1, ens1)} = thy1;
   30.57 -      val Thy {axioms = _, defs = defs2, oracles = oracles2, wrappers = (bgs2, ens2)} = thy2;
   30.58 +      val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
   30.59 +      val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
   30.60  
   30.61        val axioms' = NameSpace.empty_table;
   30.62        val defs' = Defs.merge pp (defs1, defs2);
   30.63 -      val oracles' = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   30.64 -        handle Symtab.DUP dup => err_dup_ora dup;
   30.65        val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   30.66        val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   30.67 -    in make_thy (axioms', defs', oracles', (bgs', ens')) end;
   30.68 +    in make_thy (axioms', defs', (bgs', ens')) end;
   30.69  );
   30.70  
   30.71  fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
   30.72  
   30.73 -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, wrappers}) =>
   30.74 -  make_thy (f (axioms, defs, oracles, wrappers)));
   30.75 +fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
   30.76 +  make_thy (f (axioms, defs, wrappers)));
   30.77  
   30.78  
   30.79 -fun map_axioms f = map_thy
   30.80 -  (fn (axioms, defs, oracles, wrappers) => (f axioms, defs, oracles, wrappers));
   30.81 -
   30.82 -fun map_defs f = map_thy
   30.83 -  (fn (axioms, defs, oracles, wrappers) => (axioms, f defs, oracles, wrappers));
   30.84 -
   30.85 -fun map_oracles f = map_thy
   30.86 -  (fn (axioms, defs, oracles, wrappers) => (axioms, defs, f oracles, wrappers));
   30.87 -
   30.88 -fun map_wrappers f = map_thy
   30.89 -  (fn (axioms, defs, oracles, wrappers) => (axioms, defs, oracles, f wrappers));
   30.90 +fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
   30.91 +fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
   30.92 +fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers));
   30.93  
   30.94  
   30.95  (* basic operations *)
   30.96 @@ -142,9 +125,6 @@
   30.97  val axiom_space = #1 o #axioms o rep_theory;
   30.98  val axiom_table = #2 o #axioms o rep_theory;
   30.99  
  30.100 -val oracle_space = #1 o #oracles o rep_theory;
  30.101 -val oracle_table = #2 o #oracles o rep_theory;
  30.102 -
  30.103  val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
  30.104  fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
  30.105  
  30.106 @@ -323,13 +303,4 @@
  30.107  
  30.108  end;
  30.109  
  30.110 -
  30.111 -
  30.112 -(** add oracle **)
  30.113 -
  30.114 -fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
  30.115 -  NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
  30.116 -    handle Symtab.DUP dup => err_dup_ora dup);
  30.117 -
  30.118  end;
  30.119 -
    31.1 --- a/src/Pure/thm.ML	Thu Sep 18 14:06:58 2008 +0200
    31.2 +++ b/src/Pure/thm.ML	Thu Sep 18 19:39:44 2008 +0200
    31.3 @@ -112,8 +112,8 @@
    31.4    val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
    31.5    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
    31.6    val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
    31.7 -  val invoke_oracle: theory -> xstring -> theory * Object.T -> thm
    31.8 -  val invoke_oracle_i: theory -> string -> theory * Object.T -> thm
    31.9 +  val extern_oracles: theory -> xstring list
   31.10 +  val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   31.11  end;
   31.12  
   31.13  signature THM =
   31.14 @@ -1557,36 +1557,53 @@
   31.15  
   31.16  (*** Oracles ***)
   31.17  
   31.18 -fun invoke_oracle_i thy1 name =
   31.19 -  let
   31.20 -    val oracle =
   31.21 -      (case Symtab.lookup (Theory.oracle_table thy1) name of
   31.22 -        NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
   31.23 -      | SOME (f, _) => f);
   31.24 -    val thy_ref1 = Theory.check_thy thy1;
   31.25 -  in
   31.26 -    fn (thy2, data) =>
   31.27 -      let
   31.28 -        val thy' = Theory.merge (Theory.deref thy_ref1, thy2);
   31.29 -        val (prop, T, maxidx) = Sign.certify_term thy' (oracle (thy', data));
   31.30 -        val shyps' = Sorts.insert_term prop [];
   31.31 -        val der = Deriv.oracle name prop;
   31.32 -      in
   31.33 -        if T <> propT then
   31.34 -          raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
   31.35 -        else
   31.36 -          Thm {thy_ref = Theory.check_thy thy', der = der, tags = [],
   31.37 -            maxidx = maxidx, shyps = shyps', hyps = [], tpairs = [], prop = prop}
   31.38 -      end
   31.39 +(* oracle rule *)
   31.40 +
   31.41 +fun invoke_oracle thy_ref1 name oracle arg =
   31.42 +  let val {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = rep_cterm (oracle arg) in
   31.43 +    if T <> propT then
   31.44 +      raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
   31.45 +    else
   31.46 +      Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
   31.47 +        der = Deriv.oracle name prop,
   31.48 +        tags = [],
   31.49 +        maxidx = maxidx,
   31.50 +        shyps = sorts,
   31.51 +        hyps = [],
   31.52 +        tpairs = [],
   31.53 +        prop = prop}
   31.54    end;
   31.55  
   31.56 -fun invoke_oracle thy =
   31.57 -  invoke_oracle_i thy o NameSpace.intern (Theory.oracle_space thy);
   31.58 -
   31.59 -
   31.60  end;
   31.61  end;
   31.62  end;
   31.63 +
   31.64 +
   31.65 +(* authentic derivation names *)
   31.66 +
   31.67 +fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
   31.68 +
   31.69 +structure Oracles = TheoryDataFun
   31.70 +(
   31.71 +  type T = stamp NameSpace.table;
   31.72 +  val empty = NameSpace.empty_table;
   31.73 +  val copy = I;
   31.74 +  val extend = I;
   31.75 +  fun merge _ oracles = NameSpace.merge_tables (op =) oracles
   31.76 +    handle Symtab.DUP dup => err_dup_ora dup;
   31.77 +);
   31.78 +
   31.79 +val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
   31.80 +
   31.81 +fun add_oracle (bname, oracle) thy =
   31.82 +  let
   31.83 +    val naming = Sign.naming_of thy;
   31.84 +    val name = NameSpace.full naming bname;
   31.85 +    val thy' = thy |> Oracles.map (fn (space, tab) =>
   31.86 +      (NameSpace.declare naming name space,
   31.87 +        Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
   31.88 +  in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
   31.89 +
   31.90  end;
   31.91  
   31.92  structure BasicThm: BASIC_THM = Thm;
    32.1 --- a/src/Tools/Compute_Oracle/Compute_Oracle.thy	Thu Sep 18 14:06:58 2008 +0200
    32.2 +++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Thu Sep 18 19:39:44 2008 +0200
    32.3 @@ -9,6 +9,4 @@
    32.4  uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
    32.5  begin
    32.6  
    32.7 -setup {* Compute.setup_compute *}
    32.8 -
    32.9  end
   32.10 \ No newline at end of file
    33.1 --- a/src/Tools/Compute_Oracle/compute.ML	Thu Sep 18 14:06:58 2008 +0200
    33.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Thu Sep 18 19:39:44 2008 +0200
    33.3 @@ -35,8 +35,6 @@
    33.4      (* ! *) val evaluate_prem : computer -> int -> theorem -> theorem
    33.5      (* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem
    33.6  
    33.7 -    val setup_compute : theory -> theory
    33.8 -
    33.9  end
   33.10  
   33.11  structure Compute :> COMPUTE = struct
   33.12 @@ -362,8 +360,6 @@
   33.13  (* An oracle for exporting theorems; must only be accessible from inside this structure! *)
   33.14  (* ------------------------------------------------------------------------------------- *)
   33.15  
   33.16 -exception ExportThm of term list * sort list * term
   33.17 -
   33.18  fun merge_hyps hyps1 hyps2 = 
   33.19  let
   33.20      fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab
   33.21 @@ -375,7 +371,8 @@
   33.22  
   33.23  fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
   33.24  
   33.25 -fun export_oracle (thy, ExportThm (hyps, shyps, prop)) =
   33.26 +val (_, export_oracle) = Context.>>> (Context.map_theory_result
   33.27 +  (Thm.add_oracle ("compute", fn (thy, hyps, shyps, prop) =>
   33.28      let
   33.29          val shyptab = add_shyps shyps Sorttab.empty
   33.30          fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
   33.31 @@ -385,15 +382,12 @@
   33.32          val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
   33.33          val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
   33.34      in
   33.35 -        fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop
   33.36 -    end
   33.37 -  | export_oracle _ = raise Match
   33.38 -
   33.39 -val setup_compute = (fn thy => Theory.add_oracle ("compute", export_oracle) thy)
   33.40 +        Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
   33.41 +    end)));
   33.42  
   33.43  fun export_thm thy hyps shyps prop =
   33.44      let
   33.45 -        val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop))
   33.46 +        val th = export_oracle (thy, hyps, shyps, prop)
   33.47          val hyps = map (fn h => assume (cterm_of thy h)) hyps
   33.48      in
   33.49          fold (fn h => fn p => implies_elim p h) hyps th 
    34.1 --- a/src/Tools/nbe.ML	Thu Sep 18 14:06:58 2008 +0200
    34.2 +++ b/src/Tools/nbe.ML	Thu Sep 18 19:39:44 2008 +0200
    34.3 @@ -403,15 +403,9 @@
    34.4  
    34.5  (* evaluation oracle *)
    34.6  
    34.7 -exception Norm of term * Code_Thingol.program
    34.8 -  * (Code_Thingol.typscheme * Code_Thingol.iterm) * string list;
    34.9 -
   34.10 -fun norm_oracle (thy, Norm (t, program, vs_ty_t, deps)) =
   34.11 -  Logic.mk_equals (t, eval thy t program vs_ty_t deps);
   34.12 -
   34.13 -fun norm_invoke thy t program vs_ty_t deps =
   34.14 -  Thm.invoke_oracle_i thy "HOL.norm" (thy, Norm (t, program, vs_ty_t, deps));
   34.15 -  (*FIXME get rid of hardwired theory name*)
   34.16 +val (_, norm_oracle) = Context.>>> (Context.map_theory_result
   34.17 +  (Thm.add_oracle ("norm", fn (thy, t, program, vs_ty_t, deps) =>
   34.18 +    Thm.cterm_of thy (Logic.mk_equals (t, eval thy t program vs_ty_t deps)))));
   34.19  
   34.20  fun add_triv_classes thy =
   34.21    let
   34.22 @@ -425,7 +419,7 @@
   34.23  fun norm_conv ct =
   34.24    let
   34.25      val thy = Thm.theory_of_cterm ct;
   34.26 -    fun evaluator' t program vs_ty_t deps = norm_invoke thy t program vs_ty_t deps;
   34.27 +    fun evaluator' t program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
   34.28      fun evaluator t = (add_triv_classes thy t, evaluator' t);
   34.29    in Code_Thingol.eval_conv thy evaluator ct end;
   34.30  
   34.31 @@ -455,8 +449,8 @@
   34.32    let val ctxt = Toplevel.context_of state
   34.33    in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
   34.34  
   34.35 -val setup = Theory.add_oracle ("norm", norm_oracle)
   34.36 -  #> Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
   34.37 +val setup =
   34.38 +  Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
   34.39  
   34.40  local structure P = OuterParse and K = OuterKeyword in
   34.41