transfer package: add test to prevent trying to make cterms from open terms
authorhuffman
Wed, 24 Oct 2012 18:43:25 +0200
changeset 49976 e1c45d8ec175
parent 49975 faf4afed009f
child 49977 3259ea7a52af
transfer package: add test to prevent trying to make cterms from open terms
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