# HG changeset patch
# User haftmann
# Date 1242233297 -7200
# Node ID e5f8c1c420f3bade7ed2f643b35c43140289723f
# Parent  0b615ac7eeaf17cf2ce1f1330445dbf47945800d
tuned construction of term_of instances

diff -r 0b615ac7eeaf -r e5f8c1c420f3 src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Wed May 13 18:41:54 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Wed May 13 18:48:17 2009 +0200
@@ -22,9 +22,7 @@
 val pred_ref = ref (NONE : (unit -> term Predicate.pred) option);
 
 fun eval_pred thy t =
-  t 
-  |> Eval.mk_term_of (fastype_of t)
-  |> (fn t => Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy t []);
+  Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy (HOLogic.mk_term_of (fastype_of t) t) [];
 
 fun eval_pred_elems thy t T length =
   t |> eval_pred thy |> yieldn length |> fst |> HOLogic.mk_list T;