# HG changeset patch
# User huffman
# Date 1351097005 -7200
# Node ID e1c45d8ec175f306e715a490efe4550af3782801
# Parent  faf4afed009fd1b4b67d7ec098579f5838425762
transfer package: add test to prevent trying to make cterms from open terms

diff -r faf4afed009f -r e1c45d8ec175 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Wed Oct 24 18:43:25 2012 +0200
+++ b/src/HOL/Tools/transfer.ML	Wed Oct 24 18:43:25 2012 +0200
@@ -262,7 +262,7 @@
           (Abs (x, dummyT, t'), ctxt)
         end
       | skeleton (tu as (t $ u)) ctxt =
-        if is_rhs tu then dummy ctxt else
+        if is_rhs tu andalso not (Term.is_open tu) then dummy ctxt else
         let
           val (t', ctxt) = skeleton t ctxt
           val (u', ctxt) = skeleton u ctxt