src/Tools/atomize_elim.ML
changeset 30515 bca05b17b618
parent 30510 4120fc59dd85
child 31902 862ae16a799d
--- a/src/Tools/atomize_elim.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Tools/atomize_elim.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -131,9 +131,9 @@
       THEN (CONVERSION (full_atomize_elim_conv ctxt) i)
     end)
 
-val setup = Method.add_methods
-  [("atomize_elim", Method.ctxt_args (SIMPLE_METHOD' o atomize_elim_tac),
-    "convert obtains statement to atomic object logic goal")]
+val setup =
+  Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac))
+    "convert obtains statement to atomic object logic goal"
   #> AtomizeElimData.setup
 
 end