# HG changeset patch
# User kuncar
# Date 1430567886 -7200
# Node ID 17ff843807cbf24153ce8bd226be86e3f5b1854c
# Parent  89d500d7e3eb4ee3e8617cd34c6cbed59fb6b9e6
more readable error message if some types do not correspond to sort constraints of the datatype

diff -r 89d500d7e3eb -r 17ff843807cb src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
@@ -495,6 +495,18 @@
               Raw_Simplifier.rewrite_goal_tac ctxt simp_rules, rtac TrueI ]] i
         end
     end
+    
+    (* stolen from bnf_fp_n2m.ML *)
+    fun force_typ ctxt T =
+      Term.map_types Type_Infer.paramify_vars
+      #> Type.constraint T
+      #> singleton (Type_Infer_Context.infer_types ctxt);
+
+    (* The following tests that types in rty have corresponding arities imposed by constraints of
+       the datatype fp. Otherwise rep_isom_code_tac could fail (especially transfer in it) is such
+       a way that it is not easy to infer the problem with sorts.
+    *)
+    val _ = yield_singleton (mk_Frees "x") (#T fp) lthy |> fst |> force_typ lthy qty
 
     val rep_isom_code = Goal.prove_sorry lthy [] [] rep_isom_code_goal
       (fn {context = ctxt, prems = _} => rep_isom_code_tac ctr_sugar ctxt 1)