diff -r 2b58d7b139d6 -r 907efc894051 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 28 22:42:18 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 28 23:44:41 2013 +0100
@@ -571,11 +571,10 @@
     val (thms', extra_thms) = f thms
   in (is ~~ thms') @ map (pair ~1) extra_thms end
 
-fun unfold2 ithms ctxt =
+fun unfold2 ctxt ithms =
   ithms
   |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
   |> burrow_ids add_nat_embedding
-  |> rpair ctxt
 
 
 
@@ -594,11 +593,11 @@
 fun add_extra_norm (cs, norm) =
   Extra_Norms.map (SMT_Utils.dict_update (cs, norm))
 
-fun apply_extra_norms ithms ctxt =
+fun apply_extra_norms ctxt ithms =
   let
     val cs = SMT_Config.solver_class_of ctxt
     val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
-  in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
+  in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end
 
 local
   val ignored = member (op =) [@{const_name All}, @{const_name Ex},
@@ -622,12 +621,12 @@
     in (fn t => collect t Symtab.empty) end
 in
 
-fun monomorph xthms ctxt =
+fun monomorph ctxt xthms =
   let val (xs, thms) = split_list xthms
   in
-    (map (pair 1) thms, ctxt)
-    |-> Monomorph.monomorph schematic_consts_of
-    |>> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
+    map (pair 1) thms
+    |> Monomorph.monomorph schematic_consts_of ctxt
+    |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
   end
 
 end
@@ -636,10 +635,10 @@
   iwthms
   |> gen_normalize ctxt
   |> unfold1 ctxt
+  |> monomorph ctxt
+  |> unfold2 ctxt
+  |> apply_extra_norms ctxt
   |> rpair ctxt
-  |-> monomorph
-  |-> unfold2
-  |-> apply_extra_norms
 
 val setup = Context.theory_map (
   setup_atomize #>