# 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