--- 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 ()