src/HOL/ex/Predicate_Compile.thy
changeset 31225 df6945ac4193
parent 31217 c025f32afd4e
child 32308 c2b74affab85
child 32340 b4632820e74c
--- 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