src/HOL/Code_Setup.thy
changeset 27103 d8549f4d900b
parent 26975 103dca19ef2e
child 27454 fb6a272fe5d0
     1.1 --- a/src/HOL/Code_Setup.thy	Tue Jun 10 15:30:01 2008 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Tue Jun 10 15:30:06 2008 +0200
     1.3 @@ -126,8 +126,18 @@
     1.4  
     1.5  subsection {* Evaluation oracle *}
     1.6  
     1.7 +ML {*
     1.8 +structure Eval_Method =
     1.9 +struct
    1.10 +
    1.11 +val eval_ref : (unit -> bool) option ref = ref NONE;
    1.12 +
    1.13 +end;
    1.14 +*}
    1.15 +
    1.16  oracle eval_oracle ("term") = {* fn thy => fn t => 
    1.17 -  if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
    1.18 +  if CodeTarget.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
    1.19 +    (HOLogic.dest_Trueprop t) [] 
    1.20    then t
    1.21    else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    1.22  *}