# HG changeset patch
# User haftmann
# Date 1186472328 -7200
# Node ID 605f664d5115ceb7ac0d7a6b8cce18de0553cce5
# Parent  911b46812018aab54756e604ed7130d961ed4c3f
more robust simproces

diff -r 911b46812018 -r 605f664d5115 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Tue Aug 07 09:38:47 2007 +0200
+++ b/src/HOL/Bali/Eval.thy	Tue Aug 07 09:38:48 2007 +0200
@@ -965,7 +965,7 @@
 simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = {*
   fn _ => fn _ => fn ct =>
     (case Thm.term_of ct of
-      (_ $ _ $ (Const ("Pair", _) $ (Const ("Datatype.option.None",_)) $ _) $ _  $ _ $ _) => NONE
+      (_ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name None}, _)) $ _) $ _  $ _ $ _) => NONE
     | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
 *}
 
@@ -985,11 +985,10 @@
 simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = {*
   fn _ => fn _ => fn ct =>
     (case Thm.term_of ct of
-      (_ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _)) => NONE
+      (_ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some}, _) $ _)$ _)) => NONE
     | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
 *}
 
-
 lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
 apply (case_tac "s", case_tac "a = None")
 by (auto intro!: eval.Lit)
diff -r 911b46812018 -r 605f664d5115 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Tue Aug 07 09:38:47 2007 +0200
+++ b/src/HOL/Bali/Evaln.thy	Tue Aug 07 09:38:48 2007 +0200
@@ -360,7 +360,7 @@
 simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {*
   fn _ => fn _ => fn ct =>
     (case Thm.term_of ct of
-      (_ $ _ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _))
+      (_ $ _ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some},_) $ _)$ _))
         => NONE
     | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
 *}