src/HOL/HOL.thy
changeset 30947 dd551284a300
parent 30929 d9343c0aac11
child 30966 55104c664185
     1.1 --- a/src/HOL/HOL.thy	Fri Apr 17 14:29:55 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Apr 17 14:29:56 2009 +0200
     1.3 @@ -1885,7 +1885,7 @@
     1.4      val t = Thm.term_of ct;
     1.5      val dummy = @{cprop True};
     1.6    in case try HOLogic.dest_Trueprop t
     1.7 -   of SOME t' => if Code_ML.eval_term
     1.8 +   of SOME t' => if Code_ML.eval NONE
     1.9           ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
    1.10         then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
    1.11         else dummy