# HG changeset patch
# User blanchet
# Date 1428420295 -7200
# Node ID c8860ec6fc80bf362427c34e16e6b7bf4d957a20
# Parent  09317aff0ff9df9a7536bc858fcc07f0c8f2cb24
generalized slightly

diff -r 09317aff0ff9 -r c8860ec6fc80 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Apr 07 15:14:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Apr 07 17:24:55 2015 +0200
@@ -1974,7 +1974,7 @@
           let
             fun add_edges i =
               fold (fn T => fold_index (fn (j, X) =>
-                exists_subtype (curry (op =) X) T ? cons (i, j)) Xs);
+                Term.exists_subtype (curry (op =) X) T ? cons (i, j)) Xs);
           in
             fold_index (uncurry (fold o add_edges)) ctrXs_Tsss []
           end;
diff -r 09317aff0ff9 -r c8860ec6fc80 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Apr 07 15:14:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Apr 07 17:24:55 2015 +0200
@@ -51,8 +51,8 @@
   val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
     typ list -> term -> term
   val massage_nested_corec_call: Proof.context -> (term -> bool) ->
-    (typ list -> typ -> typ -> term -> term) -> (typ -> typ -> term) -> typ list -> typ -> term ->
-    term
+    (typ list -> typ -> typ -> term -> term) -> (typ -> typ -> term -> term) -> typ list -> typ ->
+    term -> term
   val expand_to_ctr_term: Proof.context -> string -> typ list -> term -> term
   val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
     typ list -> term -> term
@@ -314,7 +314,7 @@
         (Type (@{type_name fun}, [T1, T2])) t =
         Abs (Name.uu, T1, massage_mutual_call bound_Ts U2 T2 (incr_boundvars 1 t $ Bound 0))
       | massage_mutual_call bound_Ts U T t =
-        if has_call t then massage_call bound_Ts T U t else wrap_noncall T U $ t;
+        if has_call t then massage_call bound_Ts T U t else wrap_noncall T U t;
 
     fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
         (case try (dest_map ctxt s) t of
@@ -383,11 +383,11 @@
               | _ => massage_mutual_call bound_Ts U T t))
           | _ => ill_formed_corec_call ctxt t)
         else
-          wrap_noncall T U $ t) bound_Ts;
+          wrap_noncall T U t) bound_Ts;
 
     val T = fastype_of1 (bound_Ts, t0);
   in
-    if has_call t0 then massage_any_call bound_Ts U T t0 else wrap_noncall T U $ t0
+    if has_call t0 then massage_any_call bound_Ts U T t0 else wrap_noncall T U t0
   end;
 
 fun expand_to_ctr_term ctxt s Ts t =
@@ -564,7 +564,7 @@
 fun abstract vs =
   let
     fun abs n (t $ u) = abs n t $ abs n u
-      | abs n (Abs (v, T, b)) = Abs (v, T, abs (n + 1) b)
+      | abs n (Abs (s, T, t)) = Abs (s, T, abs (n + 1) t)
       | abs n t =
         let val j = find_index (curry (op =) t) vs in
           if j < 0 then t else Bound (n + j)
@@ -603,16 +603,16 @@
   Disc of coeqn_data_disc |
   Sel of coeqn_data_sel;
 
-fun is_free_in frees (Free (v, _)) = member (op =) frees v
+fun is_free_in frees (Free (s, _)) = member (op =) frees s
   | is_free_in _ _ = false;
 
-fun is_catch_all_prem (Free (v, _)) = v = Name.uu_
+fun is_catch_all_prem (Free (s, _)) = s = Name.uu_
   | is_catch_all_prem _ = false;
 
 fun add_extra_frees ctxt frees names =
-  fold_aterms (fn x as Free (v, _) =>
-    (not (member (op =) frees x) andalso not (member (op =) names v) andalso
-     not (Variable.is_fixed ctxt v) andalso not (is_catch_all_prem x))
+  fold_aterms (fn x as Free (s, _) =>
+    (not (member (op =) frees x) andalso not (member (op =) names s) andalso
+     not (Variable.is_fixed ctxt s) andalso not (is_catch_all_prem x))
     ? cons x | _ => I);
 
 fun check_extra_frees ctxt frees names t =
@@ -901,7 +901,7 @@
               SOME (U1, U2) => if U1 = T then U2 else invalid_map ctxt t0
             | NONE => invalid_map ctxt t0);
 
-          fun rewrite bound_Ts (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) b)
+          fun rewrite bound_Ts (Abs (s, T', t')) = Abs (s, T', rewrite (T' :: bound_Ts) t')
             | rewrite bound_Ts (t as _ $ _) =
               let val (u, vs) = strip_comb t in
                 if is_Free u andalso has_call u then
@@ -919,7 +919,7 @@
             rewrite bound_Ts t0
           end;
 
-      fun wrap_noncall T U = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U);
+      fun wrap_noncall T U t = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t;
 
       val bound_Ts = List.rev (map fastype_of fun_args);