src/Pure/Isar/attrib.ML

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