--- a/Unused.thy	Mon Nov 09 13:47:46 2009 +0100
+++ b/Unused.thy	Mon Nov 09 15:23:33 2009 +0100
@@ -86,3 +86,10 @@
   apply (metis)
   done
 
+ML {*
+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 true [th] ctxt;
+  in th' end);
+*}