# 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 \<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] *)
 
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\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (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 \<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]