# HG changeset patch
# User berghofe
# Date 838980889 -7200
# Node ID 71e51870cc9a636e5e17358463645e87a0099317
# Parent  df4e40b9ff6d4cf3a0e2ef0cdae5033b5accf63a
Replaced prove_case_cong by Konrad Slinds optimized version.

diff -r df4e40b9ff6d -r 71e51870cc9a src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Tue Jul 30 18:05:22 1996 +0200
+++ b/src/HOL/datatype.ML	Fri Aug 02 12:14:49 1996 +0200
@@ -713,6 +713,7 @@
   
 (*---------------------------------------------------------------------------
  * Proves the result of "build_case_cong". 
+ * This one solves it a disjunct at a time, and builds the ss only once.
  *---------------------------------------------------------------------------*)
 fun prove_case_cong nchotomy case_rewrites ctm =
  let val {sign,t,...} = rep_cterm ctm
@@ -720,11 +721,13 @@
      val (Const("Trueprop",_) $ (Const("op =",_) $ _ $ Ma)) = tm
      val (Free(str,_)) = Ma
      val thm = prove_goalw_cterm[] ctm
-              (fn prems =>
-               [simp_tac (HOL_ss addsimps [hd prems]) 1,
-                cut_inst_tac [("x",str)] (nchotomy RS spec) 1,
-                REPEAT (SOMEGOAL (etac disjE ORELSE' etac exE)),
-                ALLGOALS(asm_simp_tac(HOL_ss addsimps (prems@case_rewrites)))])
+      (fn prems => 
+        let val simplify = asm_simp_tac(HOL_ss addsimps (prems@case_rewrites))
+        in [simp_tac (HOL_ss addsimps [hd prems]) 1,
+            cut_inst_tac [("x",str)] (nchotomy RS spec) 1,
+            REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
+            REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
+        end) 
  in standard (thm RS eq_reflection)
  end
  handle _ => raise DTYPE_ERR{func="prove_case_cong",mesg="failed"};