1.1 --- a/src/HOL/Code_Setup.thy	Thu Sep 18 14:06:58 2008 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Thu Sep 18 19:39:44 2008 +0200
     1.3 @@ -129,17 +129,22 @@
     1.4  end;
     1.5  *}
     1.6  
     1.7 -oracle eval_oracle ("term") = {* fn thy => fn t => 
     1.8 -  if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
     1.9 -    (HOLogic.dest_Trueprop t) [] 
    1.10 -  then t
    1.11 -  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    1.12 +oracle eval_oracle = {* fn ct =>
    1.13 +  let
    1.14 +    val thy = Thm.theory_of_cterm ct;
    1.15 +    val t = Thm.term_of ct;
    1.16 +  in
    1.17 +    if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
    1.18 +      (HOLogic.dest_Trueprop t) [] 
    1.19 +    then ct
    1.20 +    else @{cprop True} (*dummy*)
    1.21 +  end
    1.22  *}
    1.23  
    1.24  method_setup eval = {*
    1.25  let
    1.26    fun eval_tac thy = 
    1.27 -    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
    1.28 +    CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
    1.29  in 
    1.30    Method.ctxt_args (fn ctxt => 
    1.31      Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))