Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
transfer package: add test to prevent trying to make cterms from open terms
authorhuffman
Wed, 24 Oct 2012 18:43:25 +0200
changeset 50991e1c45d8ec175
parent 50990 faf4afed009f
child 50992 3259ea7a52af
transfer package: add test to prevent trying to make cterms from open terms
src/HOL/Tools/transfer.ML file | annotate | diff | comparison | revisions 
     1.1 --- a/src/HOL/Tools/transfer.ML	Wed Oct 24 18:43:25 2012 +0200
     1.2 +++ b/src/HOL/Tools/transfer.ML	Wed Oct 24 18:43:25 2012 +0200
     1.3 @@ -262,7 +262,7 @@
     1.4            (Abs (x, dummyT, t'), ctxt)
     1.5          end
     1.6        | skeleton (tu as (t $ u)) ctxt =
     1.7 -        if is_rhs tu then dummy ctxt else
     1.8 +        if is_rhs tu andalso not (Term.is_open tu) then dummy ctxt else
     1.9          let
    1.10            val (t', ctxt) = skeleton t ctxt
    1.11            val (u', ctxt) = skeleton u ctxt
wneuper/isa