src/HOL/IOA/Solve.ML

  by (Fast_tac 1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (!simpset addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
-                addsplits [expand_if,expand_option_case]) 1);
+                addsplits [expand_if,split_option_case]) 1);
 qed"comp1_reachable";
 
 
 (* Exact copy of proof of comp1_reachable for the second 
    component of a parallel composition.     *)

  by (Fast_tac 1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (!simpset addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
-                addsplits [expand_if,expand_option_case]) 1);
+                addsplits [expand_if,split_option_case]) 1);
 qed"comp2_reachable";
 
 
 (* Composition of possibility-mappings *)
 

 by (Simp_tac 1);
 (* execution is indeed an execution of C *)
 by (asm_full_simp_tac
       (!simpset addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,rename_def]
-                addsplits [expand_option_case]) 1);
+                addsplits [split_option_case]) 1);
 by (best_tac (!claset addSDs [spec] addDs [sym] addss (!simpset)) 1);
 qed"reachable_rename_ioa";
 
 
 goal Solve.thy "!!f.[| is_weak_pmap f C A |]\