src/HOL/Bali/Evaln.thy

   fun is_Inj (Const (inj,_) $ _) = true
     | is_Inj _                   = false
   fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ 
     (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
 in
-  make_simproc name lhs pred (thm name)
+  cond_simproc name lhs pred (thm name)
 end;
 
 val evaln_expr_proc = enf "expr" "In1l" "\<exists>v.  w=In1 v  \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s'";
 val evaln_var_proc  = enf "var"  "In2"  "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s'";
 val evaln_exprs_proc= enf "exprs""In3"  "\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s'";

   fun pred (_ $ (Const ("Pair",_) $
      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
        (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
 in
   val evaln_abrupt_proc = 
- make_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
+ cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
 end;
 Addsimprocs [evaln_abrupt_proc]
 *}
 
 lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"