# HG changeset patch
# User haftmann
# Date 1391955993 -3600
# Node ID b7c061e1d817ecd9acf069fcc9086b14a1d7ae75
# Parent  5e5c36b051af516ebfacd7246fb8816836490658
tuned

diff -r 5e5c36b051af -r b7c061e1d817 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Feb 09 13:07:23 2014 +0100
+++ b/src/Pure/Isar/code.ML	Sun Feb 09 15:26:33 2014 +0100
@@ -906,11 +906,14 @@
     val rewrite = Conv.fconv_rule (conv (Simplifier.rewrite (put_simpset ss ctxt)));
   in singleton (Variable.trade (K (map rewrite)) ctxt) end;
 
+fun preprocess thy conv ss =
+  Thm.transfer thy
+  #> rewrite_eqn thy conv ss
+  #> Axclass.unoverload thy
+
 fun cert_of_eqns_preprocess thy functrans ss c =
-  (map o apfst) (Thm.transfer thy)
-  #> perhaps (perhaps_loop (perhaps_apply functrans))
-  #> (map o apfst) (rewrite_eqn thy eqn_conv ss) 
-  #> (map o apfst) (Axclass.unoverload thy)
+  perhaps (perhaps_loop (perhaps_apply functrans))
+  #> (map o apfst) (preprocess thy eqn_conv ss)
   #> cert_of_eqns thy c;
 
 fun get_cert thy { functrans, ss } c =
@@ -922,9 +925,7 @@
     | None => nothing_cert thy c
     | Proj (_, tyco) => cert_of_proj thy c tyco
     | Abstr (abs_thm, tyco) => abs_thm
-        |> Thm.transfer thy
-        |> rewrite_eqn thy Conv.arg_conv ss
-        |> Axclass.unoverload thy
+        |> preprocess thy Conv.arg_conv ss
         |> cert_of_abs thy tyco c;