Merge

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 05 17:06:11 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 05 17:07:22 2014 +0000
@@ -63,11 +63,11 @@
     (fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar)));
 
 fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
-  | unfold_let (Const (@{const_name prod_case}, _) $ t) =
-    (case unfold_let t of
-      t' as Abs (s1, T1, Abs (s2, T2, _)) =>
-      let val v = Var ((s1 ^ s2, Term.maxidx_of_term t' + 1), HOLogic.mk_prodT (T1, T2)) in
-        lambda v (incr_boundvars 1 (betapplys (t', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
+  | unfold_let (t as Const (@{const_name prod_case}, _) $ u) =
+    (case unfold_let u of
+      u' as Abs (s1, T1, Abs (s2, T2, _)) =>
+      let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
+        lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
       end
     | _ => t)
   | unfold_let (t $ u) = betapply (unfold_let t, unfold_let u)

--- a/src/Pure/Tools/simplifier_trace.ML	Wed Feb 05 17:06:11 2014 +0000
+++ b/src/Pure/Tools/simplifier_trace.ML	Wed Feb 05 17:07:22 2014 +0000
@@ -48,15 +48,15 @@
      breakpoints = empty_breakpoints}
   val extend = I
   fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1,
-              breakpoints = breakpoints1, ...},
+              breakpoints = breakpoints1, ...}: T,
              {max_depth = max_depth2, mode = mode2, interactive = interactive2,
-              breakpoints = breakpoints2, ...}) =
+              breakpoints = breakpoints2, ...}: T) =
     {max_depth = Int.max (max_depth1, max_depth2),
      depth = 0,
      mode = merge_modes mode1 mode2,
      interactive = interactive1 orelse interactive2,
      parent = 0,
-     breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}
+     breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T
 )
 
 fun map_breakpoints f_term f_thm =
@@ -191,7 +191,9 @@
   end
 
 
-fun step {term, thm, unconditional, ctxt, rrule} =
+type data = {term: term, thm: thm, unconditional: bool, ctxt: Proof.context, rrule: rrule}
+
+fun step ({term, thm, unconditional, ctxt, rrule}: data) =
   let
     val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
 
@@ -292,7 +294,7 @@
           (output_result res; put (#1 res))
   in Context.the_proof context' end
 
-fun indicate_failure {term, ctxt, thm, rrule, ...} ctxt' =
+fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' =
   let
     fun payload () =
       let