src/HOL/UNITY/Simple/NSP_Bad.thy

--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Wed Nov 29 15:44:51 2006 +0100
@@ -129,8 +129,7 @@
 
 method_setup ns_induct = {*
     Method.ctxt_args (fn ctxt =>
-        Method.METHOD (fn facts =>
-            ns_induct_tac (local_clasimpset_of ctxt) 1)) *}
+        Method.SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
     "for inductive reasoning about the Needham-Schroeder protocol"
 
 text{*Converts invariants into statements about reachable states*}