# HG changeset patch
# User traytel
# Date 1452587288 -3600
# Node ID b8dc1fd7d90050b5ba6937fea6bbfa0b6e41cc9d
# Parent  c92d82c3f41bf7c632cdff32b9f427445ddda6b1
more careful witness' type analysis

diff -r c92d82c3f41b -r b8dc1fd7d900 src/HOL/Datatype_Examples/Lift_BNF.thy
--- a/src/HOL/Datatype_Examples/Lift_BNF.thy	Tue Jan 12 09:28:08 2016 +0100
+++ b/src/HOL/Datatype_Examples/Lift_BNF.thy	Tue Jan 12 09:28:08 2016 +0100
@@ -72,4 +72,10 @@
 
 copy_bnf 'a myopt via myopt_type_def
 
+typedef ('k, 'v) fmap = "{M :: ('k \<rightharpoonup> 'v). finite (dom M)}"
+  by (rule exI[of _ Map.empty]) simp_all
+
+lift_bnf (dead 'k, 'v) fmap [wits: "Map.empty :: 'k \<Rightarrow> 'v option"]
+  by auto
+
 end
diff -r c92d82c3f41b -r b8dc1fd7d900 src/HOL/Tools/BNF/bnf_lift.ML
--- a/src/HOL/Tools/BNF/bnf_lift.ML	Tue Jan 12 09:28:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Tue Jan 12 09:28:08 2016 +0100
@@ -145,8 +145,14 @@
     (* val wit_closed_F = @{term "wit_F a \<in> F"}; *)
     val (var_as, names_lthy) = mk_Frees "a" alphas names_lthy;
     val (var_bs, _) = mk_Frees "a" alphas names_lthy;
+    fun binder_types_until_eq V T =
+      let
+        fun strip (TU as Type ("fun", [T, U])) = if V = TU then [] else T :: strip U
+          | strip T = if V = T then [] else
+              error ("Bad type for witness: " ^ quote (Syntax.string_of_typ lthy T));
+      in strip T end;
     val Iwits = the_default wits_F (Option.map (map (`(map (fn T =>
-      find_index (fn U => T = U) alphas) o fst o strip_type o fastype_of))) wits);
+      find_index (fn U => T = U) alphas) o binder_types_until_eq RepT o fastype_of))) wits);
     val wit_closed_Fs =
       Iwits |> map (fn (I, wit_F) =>
         let