# HG changeset patch
# User haftmann
# Date 1242926122 -7200
# Node ID df6945ac4193208197a69cc29ae36755c387e4f2
# Parent  6f4fb815439abbe297e17e4372d8cc1525596dac
using precompiled Predicate.map

diff -r 6f4fb815439a -r df6945ac4193 src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Thu May 21 16:51:00 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Thu May 21 19:15:22 2009 +0200
@@ -24,7 +24,7 @@
     val T2 = T1 --> mk_predT T --> mk_predT @{typ term};
     val t' = Const (@{const_name Predicate.map}, T2) (*FIXME*)
       $ Const (@{const_name Code_Eval.term_of}, T1) $ t;
-  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) @{code Predicate.map} thy t' []) end;
+  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
 
 fun values ctxt k t_compr =
   let