src/HOL/HOL.thy
changeset 30970 3fe2e418a071
parent 30966 55104c664185
child 30980 fe0855471964
     1.1 --- a/src/HOL/HOL.thy	Fri Apr 24 08:24:52 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Apr 24 08:24:54 2009 +0200
     1.3 @@ -1889,7 +1889,7 @@
     1.4      val dummy = @{cprop True};
     1.5    in case try HOLogic.dest_Trueprop t
     1.6     of SOME t' => if Code_ML.eval NONE
     1.7 -         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
     1.8 +         ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] 
     1.9         then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
    1.10         else dummy
    1.11      | NONE => dummy