src/HOL/UNITY/Simple/NSP_Bad.thy

--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu Jul 23 18:44:09 2009 +0200
@@ -125,7 +125,7 @@
 
 method_setup ns_induct = {*
     Scan.succeed (fn ctxt =>
-        SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
+        SIMPLE_METHOD' (ns_induct_tac (clasimpset_of ctxt))) *}
     "for inductive reasoning about the Needham-Schroeder protocol"
 
 text{*Converts invariants into statements about reachable states*}