# HG changeset patch
# User nipkow
# Date 878547455 -3600
# Node ID 4747aefbbc52958c6d95721136d70890dac57a46
# Parent  3a6e1e562aede0bd0442cbcc10ad5b36d66d707a
expand_option_case -> split_option_case

diff -r 3a6e1e562aed -r 4747aefbbc52 src/HOL/IOA/Solve.ML
--- a/src/HOL/IOA/Solve.ML	Mon Nov 03 08:16:35 1997 +0100
+++ b/src/HOL/IOA/Solve.ML	Mon Nov 03 09:57:35 1997 +0100
@@ -78,7 +78,7 @@
 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";
 
 
@@ -98,7 +98,7 @@
 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";
 
 
@@ -160,7 +160,7 @@
 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";
 
diff -r 3a6e1e562aed -r 4747aefbbc52 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Mon Nov 03 08:16:35 1997 +0100
+++ b/src/HOL/Map.ML	Mon Nov 03 09:57:35 1997 +0100
@@ -26,21 +26,21 @@
 goalw thy [override_def] "empty ++ m = m";
 by(Simp_tac 1);
 br ext 1;
-by(split_tac [expand_option_case] 1);
+by(split_tac [split_option_case] 1);
 by(Simp_tac 1);
 qed "empty_override";
 Addsimps [empty_override];
 
 goalw thy [override_def]
  "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
-by(simp_tac (!simpset addsplits [expand_option_case]) 1);
+by(simp_tac (!simpset addsplits [split_option_case]) 1);
 qed_spec_mp "override_Some_iff";
 
 bind_thm("override_SomeD", standard(override_Some_iff RS iffD1));
 
 goalw thy [override_def]
  "((m ++ n) k = None) = (n k = None & m k = None)";
-by(simp_tac (!simpset addsplits [expand_option_case]) 1);
+by(simp_tac (!simpset addsplits [split_option_case]) 1);
 qed "override_None";
 AddIffs [override_None];
 
@@ -48,7 +48,7 @@
 by(induct_tac "xs" 1);
 by(Simp_tac 1);
 br ext 1;
-by(asm_simp_tac (!simpset addsplits [expand_if,expand_option_case]) 1);
+by(asm_simp_tac (!simpset addsplits [expand_if,split_option_case]) 1);
 qed "map_of_append";
 Addsimps [map_of_append];
 
diff -r 3a6e1e562aed -r 4747aefbbc52 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Mon Nov 03 08:16:35 1997 +0100
+++ b/src/HOL/Option.ML	Mon Nov 03 09:57:35 1997 +0100
@@ -5,5 +5,3 @@
 
 Derived rules
 *)
-
-val expand_option_case = split_option_case;
diff -r 3a6e1e562aed -r 4747aefbbc52 src/HOL/Subst/Unify.ML
--- a/src/HOL/Subst/Unify.ML	Mon Nov 03 08:16:35 1997 +0100
+++ b/src/HOL/Subst/Unify.ML	Mon Nov 03 09:57:35 1997 +0100
@@ -161,7 +161,7 @@
 			inv_image_def, less_eq]) 1);
 (** LEVEL 7 **)
 (*Comb-Comb case*)
-by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
+by (asm_simp_tac (!simpset addsplits [split_option_case]) 1);
 by (strip_tac 1);
 by (rtac (trans_unifyRel RS transD) 1);
 by (Blast_tac 1);
@@ -184,7 +184,7 @@
 \                            of None => None    \
 \                             | Some sigma => Some (theta <> sigma)))";
 by (asm_simp_tac (!simpset addsimps (unify_TC::unifyRules0)
-			   addsplits [expand_option_case]) 1);
+			   addsplits [split_option_case]) 1);
 qed "unifyCombComb";
 
 
@@ -220,7 +220,7 @@
 by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
 (** LEVEL 8 **)
 (*Comb-Comb case*)
-by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
+by (asm_simp_tac (!simpset addsplits [split_option_case]) 1);
 by (strip_tac 1);
 by (rotate_tac ~2 1);
 by (asm_full_simp_tac 
@@ -246,7 +246,7 @@
 by (ALLGOALS 
     (asm_simp_tac 
        (!simpset addsimps [Var_Idem] 
-	         addsplits [expand_if,expand_option_case])));
+	         addsplits [expand_if,split_option_case])));
 (*Comb-Comb case*)
 by (safe_tac (!claset));
 by (REPEAT (dtac spec 1 THEN mp_tac 1));