# HG changeset patch
# User lcp
# Date 799514538 -7200
# Node ID 08fda51489713491007b79dd3ca56a7db52b2516
# Parent  a203181678d3a9d76bf5fd6cd30dc613d06c5caf
prove_case_equation now calls uses meta_eq_to_obj_eq to cope
with new form of 'split'.  Tried calling simp_tac instead of using resolution
with trans, but it was significantly slower: 98.3 secs instead of 91.2 secs
for ex/Enum.

diff -r a203181678d3 -r 08fda5148971 src/ZF/constructor.ML
--- a/src/ZF/constructor.ML	Wed May 03 16:46:17 1995 +0200
+++ b/src/ZF/constructor.ML	Wed May 03 17:22:18 1995 +0200
@@ -51,20 +51,21 @@
     mk_tprop (eq_const $ (big_case_tm $ (list_comb (Const(name,T), args)))
 		         $ (list_comb (case_free, args))) ;
 
-val case_trans = hd con_defs RS def_trans;
+val case_trans = hd con_defs RS def_trans
+and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
 
 (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
 fun case_tacsf con_def _ = 
   [rewtac con_def,
    rtac case_trans 1,
-   REPEAT (resolve_tac [refl, Pr.split_eq RS trans, 
-			Su.case_inl RS trans, 
-			Su.case_inr RS trans] 1)];
+   REPEAT (resolve_tac [refl, split_trans, 
+                        Su.case_inl RS trans, 
+                        Su.case_inr RS trans] 1)];
 
 fun prove_case_equation (arg,con_def) =
     prove_goalw_cterm [] 
         (cterm_of (sign_of thy) (mk_case_equation arg))
-	(case_tacsf con_def);
+        (case_tacsf con_def);
 
 val free_iffs = 
     map standard (con_defs RL [def_swap_iff]) @