1.1 --- a/src/HOL/Tools/transfer_data.ML	Wed Jun 24 20:52:49 2009 +0200
     1.2 +++ b/src/HOL/Tools/transfer_data.ML	Wed Jun 24 21:28:02 2009 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th = 
     1.6   let 
     1.7 -  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import_thms true (map Drule.mk_term [a0, D0]) ctxt0)
     1.8 +  val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
     1.9    val (aT,bT) = 
    1.10       let val T = typ_of (ctyp_of_term a) 
    1.11       in (Term.range_type T, Term.domain_type T)