diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/NSA/StarDef.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -91,6 +91,12 @@
 use "transfer.ML"
 setup Transfer_Principle.setup
 
+method_setup transfer = {*
+  Attrib.thms >> (fn ths => fn ctxt =>
+    SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))
+*} "transfer principle"
+
+
 text {* Transfer introduction rules. *}
 
 lemma transfer_ex [transfer_intro]: