summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | traytel |

Fri, 21 Aug 2015 16:10:11 +0200 | |

changeset 61004 | 1dd6669ff612 |

parent 60993 | 531a48ae1425 |

child 61005 | 151d92332625 |

don't use types that come from the database---they are inconsistent with the ones occurring in the terms

--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Thu Aug 20 21:14:58 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Fri Aug 21 16:10:11 2015 +0200 @@ -470,12 +470,13 @@ (SOME cname, ts as _ :: _) => let val (fs, x) = split_last ts; - fun strip_abs i Us t = + fun strip_abs i t = let val zs = strip_abs_vars t; val j = length zs; val (xs, ys) = - if j < i then (zs @ map (pair "x") (drop j Us), []) + if j < i then (zs @ + map (pair "x") (drop j (take i (binder_types (fastype_of t)))), []) else chop i zs; val u = fold_rev Term.abs ys (strip_abs_body t); val xs' = map Free @@ -501,7 +502,7 @@ let val Us = binder_types U; val k = length Us; - val p as (xs, _) = strip_abs k Us t; + val p as (xs, _) = strip_abs k t; in (Const (s, map fastype_of xs ---> fastype_of x), p, is_dependent k t) end) (constructors ~~ fs);