src/HOL/Bali/Evaln.thy
changeset 24165 605f664d5115
parent 24019 67bde7cfcf10
child 24727 dd9ea6b72eb9
     1.1 --- a/src/HOL/Bali/Evaln.thy	Tue Aug 07 09:38:47 2007 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Tue Aug 07 09:38:48 2007 +0200
     1.3 @@ -360,7 +360,7 @@
     1.4  simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {*
     1.5    fn _ => fn _ => fn ct =>
     1.6      (case Thm.term_of ct of
     1.7 -      (_ $ _ $ _ $ _ $ _ $ _ $ (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _))
     1.8 +      (_ $ _ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some},_) $ _)$ _))
     1.9          => NONE
    1.10      | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
    1.11  *}