# HG changeset patch
# User blanchet
# Date 1410454476 -7200
# Node ID acc2f1801acc9a4ae875292029a8bfb937ca5976
# Parent  a0fe6d8c8ba2541a9cb41a8e797d07e57dba9809
tuning

diff -r a0fe6d8c8ba2 -r acc2f1801acc src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Sep 11 18:54:36 2014 +0200
@@ -331,7 +331,7 @@
       if has_call t then
         raise PRIMREC ("recursive call not directly applied to constructor argument", [t])
       else
-        try_nested_rec [] (head_of t) t |> the_default t
+        try_nested_rec [] (head_of t) t |> the_default t;
   in
     subst' o subst []
   end;
@@ -386,10 +386,10 @@
     val n_funs = length funs_data;
 
     val ctr_spec_eqn_data_list' =
-      (take n_funs rec_specs |> map #ctr_specs) ~~ funs_data
+      map #ctr_specs (take n_funs rec_specs) ~~ funs_data
       |> maps (uncurry (finds (fn (x, y) => #ctr x = #ctr y))
-          ##> (fn x => null x orelse
-            raise PRIMREC ("excess equations in definition", map #rhs_term x)) #> fst);
+        ##> (fn x => null x orelse
+          raise PRIMREC ("excess equations in definition", map #rhs_term x)) #> fst);
     val _ = ctr_spec_eqn_data_list' |> map (fn ({ctr, ...}, x) =>
       if length x > 1 then raise PRIMREC ("multiple equations for constructor", map #user_eqn x)
       else if length x = 1 orelse nonexhaustive then ()