# HG changeset patch
# User bulwahn
# Date 1274286248 -7200
# Node ID 25fdef26b460ede499dd52f1ff66617bb3bdb433
# Parent  842a73dc6d0ea3f3fc2520beb03544e945c81b02
removed unnecessary Thm.transfer in the predicate compiler

diff -r 842a73dc6d0e -r 25fdef26b460 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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)