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