src/HOL/Bali/Evaln.thy
changeset 24165 605f664d5115
parent 24019 67bde7cfcf10
child 24727 dd9ea6b72eb9
--- 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}))
 *}