equal
deleted
inserted
replaced
102 (case try (dest_map ctxt s) t1 of |
102 (case try (dest_map ctxt s) t1 of |
103 SOME res => res |
103 SOME res => res |
104 | NONE => |
104 | NONE => |
105 let |
105 let |
106 val thy = Proof_Context.theory_of ctxt; |
106 val thy = Proof_Context.theory_of ctxt; |
107 val map_thms = of_fp_sugar #mapss (the (fp_sugar_of ctxt s)) |
107 val map_thms = flat (#mapss (the (fp_sugar_of ctxt s))); |
108 val map_thms' = map (fn thm => thm RS sym RS eq_reflection) map_thms; |
108 val map_thms' = map (fn thm => thm RS sym RS eq_reflection) map_thms; |
109 val t' = Raw_Simplifier.rewrite_term thy map_thms' [] t; |
109 val t' = Raw_Simplifier.rewrite_term thy map_thms' [] t; |
110 in |
110 in |
111 if t aconv t' then raise Fail "dest_applied_map_or_ctr" |
111 if t aconv t' then raise Fail "dest_abs_or_applied_map_or_ctr" |
112 else dest_map ctxt s (fst (dest_comb t')) |
112 else dest_map ctxt s (fst (dest_comb t')) |
113 end); |
113 end); |
114 |
114 |
115 fun map_partition f xs = |
115 fun map_partition f xs = |
116 fold_rev (fn x => fn (ys, (good, bad)) => |
116 fold_rev (fn x => fn (ys, (good, bad)) => |