# HG changeset patch
# User blanchet
# Date 1379545765 -7200
# Node ID 9e64151359e833bcb405775f03dc5c7aa5c09a7e
# Parent  cfcb987d470001310dfb5eed834bae2cc6d691c5
simplified code

diff -r cfcb987d4700 -r 9e64151359e8 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 01:09:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 01:09:25 2013 +0200
@@ -564,13 +564,17 @@
 fun build_corec_arg_direct_call lthy has_call sel_eqns sel =
   let
     val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
-    fun rewrite is_end U _ t =
-      if U = @{typ bool} then @{term True} |> has_call t ? K @{term False} (* stop? *)
-      else if is_end = has_call t then undef_const
-      else if is_end then t (* end *)
-      else HOLogic.mk_tuple (snd (strip_comb t)); (* continue *)
-    fun massage rhs_term is_end t = massage_direct_corec_call
-      lthy has_call (rewrite is_end) [] (range_type (fastype_of t)) rhs_term;
+    fun massage rhs_term is_end t =
+      let
+        val U = range_type (fastype_of t);
+        fun rewrite t =
+          if U = @{typ bool} then (if has_call t then @{term False} else @{term True}) (* stop? *)
+          else if is_end = has_call t then undef_const
+          else if is_end then t (* end *)
+          else HOLogic.mk_tuple (snd (strip_comb t)); (* continue *)
+      in
+        massage_direct_corec_call lthy has_call rewrite U rhs_term
+      end;
   in
     if is_none maybe_sel_eqn then K I else
       abs_tuple (#fun_args (the maybe_sel_eqn)) oo massage (#rhs_term (the maybe_sel_eqn))
diff -r cfcb987d4700 -r 9e64151359e8 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 01:09:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 01:09:25 2013 +0200
@@ -53,8 +53,8 @@
 
   val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
     typ list -> term -> term -> term -> term
-  val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
-    typ list -> typ -> term -> term
+  val massage_direct_corec_call: Proof.context -> (term -> bool) -> (term -> term) -> typ -> term ->
+    term
   val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
     (typ -> typ -> term -> term) -> typ list -> typ -> term -> term
   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
@@ -126,6 +126,9 @@
   error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t));
 fun ill_formed_corec_call ctxt t =
   error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
+fun ill_formed_corec_code_rhs ctxt t =
+  error ("Ill-formed corecursive equation right-hand side: " ^
+    quote (Syntax.string_of_term ctxt t));
 fun invalid_map ctxt t =
   error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
 fun unexpected_rec_call ctxt t =
@@ -193,25 +196,23 @@
     massage_call
   end;
 
-fun massage_let_and_if ctxt check_cond massage_leaf =
+fun massage_let_and_if ctxt check_cond massage_leaf U =
   let
-    fun massage_rec U T t =
+    fun massage_rec t =
       (case Term.strip_comb t of
-        (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec U T (betapply (arg2, arg1))
+        (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1))
       | (Const (@{const_name If}, _), arg :: args) =>
-        list_comb (If_const U $ tap check_cond arg, map (massage_rec U T) args)
-      | _ => massage_leaf U T t)
+        list_comb (If_const U $ tap check_cond arg, map massage_rec args)
+      | _ => massage_leaf t)
   in
     massage_rec
   end;
 
-fun massage_direct_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
-  let val typof = curry fastype_of1 bound_Ts in
-    massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) massage_direct_call
-      res_U (typof t) t
-  end;
+fun massage_direct_corec_call ctxt has_call massage_direct_call U t =
+  massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) massage_direct_call
+    U t;
 
-fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts res_U t =
+fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts U t =
   let
     val typof = curry fastype_of1 bound_Ts;
     val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
@@ -246,7 +247,7 @@
 
     fun massage_call U T =
       massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt)
-        (fn U => fn T => fn t =>
+        (fn t =>
             (case U of
               Type (s, Us) =>
               (case try (dest_ctr ctxt s) t of
@@ -264,9 +265,9 @@
                     handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
                 | _ => check_and_massage_direct_call U T t))
             | _ => ill_formed_corec_call ctxt t))
-        U T
+        U
   in
-    massage_call res_U (typof t) t
+    massage_call U (typof t) t
   end;
 
 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;