
diff -r c6a9b4e4d548 -r 40bb0c4718a6 Unused.thy
--- 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);
+*}




