# HG changeset patch # User wenzelm # Date 1213631676 -7200 # Node ID 5a3e5e46d977ceb99bd19724302976b299738b10 # Parent b316dde851f52ea9fe526c17083254b9c13968c8 sum3_instantiate: proper context; diff -r b316dde851f5 -r 5a3e5e46d977 src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Mon Jun 16 17:54:35 2008 +0200 +++ b/src/HOL/Bali/AxSem.thy Mon Jun 16 17:54:36 2008 +0200 @@ -1013,7 +1013,7 @@ apply (auto simp add: type_ok_def) done -ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *} +ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *} declare ax_Abrupts [intro!] lemmas ax_Normal_cases = ax_cases [of _ _ _ normal] diff -r b316dde851f5 -r 5a3e5e46d977 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Mon Jun 16 17:54:35 2008 +0200 +++ b/src/HOL/Bali/Basis.thy Mon Jun 16 17:54:36 2008 +0200 @@ -228,8 +228,9 @@ "the_In1r" == "the_Inr \ the_In1" ML {* -fun sum3_instantiate thm = map (fn s => simplify(simpset()delsimps[@{thm not_None_eq}]) - (Drule.read_instantiate [("t","In"^s^" ?x")] thm)) ["1l","2","3","1r"] +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"] *} (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) diff -r b316dde851f5 -r 5a3e5e46d977 src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Mon Jun 16 17:54:35 2008 +0200 +++ b/src/HOL/Bali/Eval.thy Mon Jun 16 17:54:36 2008 +0200 @@ -891,7 +891,7 @@ | _ => SOME (mk_meta_eq @{thm eval_stmt_eq})) *} ML {* -bind_thms ("AbruptIs", sum3_instantiate @{thm eval.Abrupt}) +bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt}) *} declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!] diff -r b316dde851f5 -r 5a3e5e46d977 src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Mon Jun 16 17:54:35 2008 +0200 +++ b/src/HOL/Bali/Evaln.thy Mon Jun 16 17:54:36 2008 +0200 @@ -294,7 +294,7 @@ (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *} -ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{thm evaln.Abrupt}) *} +ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *} declare evaln_AbruptIs [intro!] lemma evaln_Callee: "G\Norm s\In1l (Callee l e)\\n\ (v,s') = False" diff -r b316dde851f5 -r 5a3e5e46d977 src/HOL/Bali/Term.thy --- a/src/HOL/Bali/Term.thy Mon Jun 16 17:54:35 2008 +0200 +++ b/src/HOL/Bali/Term.thy Mon Jun 16 17:54:36 2008 +0200 @@ -266,7 +266,7 @@ is_stmt :: "term \ bool" "is_stmt t \ \c. t=In1r c" -ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *} +ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *} declare is_stmt_rews [simp]