--- a/src/HOL/Bali/Basis.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/HOL/Bali/Basis.thy Mon Jun 16 22:13:39 2008 +0200
@@ -230,7 +230,7 @@
ML {*
fun sum3_instantiate ctxt thm = map (fn s =>
simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
- (RuleInsts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
+ (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] *)