--- a/src/HOL/Hyperreal/transfer.ML Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/Hyperreal/transfer.ML Wed Nov 29 15:44:51 2006 +0100
@@ -107,9 +107,6 @@
(fn {intros,unfolds,refolds,consts} =>
{intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
-val transfer_method = Method.thms_ctxt_args (fn ths => fn ctxt =>
- Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ctxt ths));
-
val setup =
TransferData.init #>
Attrib.add_attributes
@@ -119,6 +116,7 @@
"declaration of transfer unfolding rule"),
("transfer_refold", Attrib.add_del_args refold_add refold_del,
"declaration of transfer refolding rule")] #>
- Method.add_method ("transfer", transfer_method, "transfer principle");
+ Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt =>
+ Method.SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
end;