src/HOL/Bali/Basis.thy

--- a/src/HOL/Bali/Basis.thy	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Bali/Basis.thy	Thu Jul 23 18:44:09 2009 +0200
@@ -229,7 +229,7 @@
 
 ML {*
 fun sum3_instantiate ctxt thm = map (fn s =>
-  simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
+  simplify (simpset_of ctxt delsimps[@{thm not_None_eq}])
     (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
 *}
 (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)