1.1 --- a/src/Pure/Isar/attrib.ML	Wed Jun 24 20:52:49 2009 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Jun 24 21:28:02 2009 +0200
     1.3 @@ -265,7 +265,7 @@
     1.4  val no_vars = Thm.rule_attribute (fn context => fn th =>
     1.5    let
     1.6      val ctxt = Variable.set_body false (Context.proof_of context);
     1.7 -    val ((_, [th']), _) = Variable.import_thms true [th] ctxt;
     1.8 +    val ((_, [th']), _) = Variable.import true [th] ctxt;
     1.9    in th' end);
    1.10  
    1.11  val eta_long =