# HG changeset patch
# User blanchet
# Date 1461605000 -7200
# Node ID 2146553e96c6fbb839aa8454cdce73e3405bcf63
# Parent  8053ef5a017472d5fe8265a6358dcc6be9d35f59
generalize code to avoid making assumptions about type variable names

diff -r 8053ef5a0174 -r 2146553e96c6 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Apr 15 21:33:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Apr 25 19:23:20 2016 +0200
@@ -127,8 +127,8 @@
     val Xs_frecs = Xs ~~ frecs;
     val fss = unflat ctrss fs;
 
-    fun mk_rec_call g n (Type (@{type_name fun}, [dom_T, ran_T])) =
-        Abs (Name.uu, dom_T, mk_rec_call g (n + 1) ran_T)
+    fun mk_rec_call g n (Type (@{type_name fun}, [_, ran_T])) =
+        Abs (Name.uu, Term.dummyT, mk_rec_call g (n + 1) ran_T)
       | mk_rec_call g n X =
         let
           val frec = the (AList.lookup (op =) Xs_frecs X);
@@ -147,6 +147,7 @@
       in
         fold_rev (fold_rev Logic.all) [fs, gs]
           (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs)))
+        |> Syntax.check_term ctxt
       end;
 
     val goalss = @{map 4} (@{map 3} o mk_goal) frecs ctrXs_Tsss ctrss fss;