--- 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]
--- 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 \<circ> 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] *)
--- 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!]
--- 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\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
--- 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 \<Rightarrow> bool"
"is_stmt t \<equiv> \<exists>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]