src/HOL/Decision_Procs/ferrack_tac.ML
changeset 30510 4120fc59dd85
parent 30439 57c68b3af2ea
child 31302 12677a808d43
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -100,7 +100,7 @@
 
 fun linr_meth src =
   Method.syntax (Args.mode "no_quantify") src
-  #> (fn (q, ctxt) => Method.SIMPLE_METHOD' (linr_tac ctxt (not q)));
+  #> (fn (q, ctxt) => SIMPLE_METHOD' (linr_tac ctxt (not q)));
 
 val setup =
   Method.add_method ("rferrack", linr_meth,