--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed May 19 18:24:07 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed May 19 18:24:08 2010 +0200
@@ -241,7 +241,7 @@
val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
-fun intros_of thy = map (Thm.transfer thy) o #intros o the_pred_data thy
+fun intros_of thy = #intros o the_pred_data thy
fun the_elim_of thy name = case #elim (the_pred_data thy name)
of NONE => error ("No elimination rule for predicate " ^ quote name)