# HG changeset patch
# User schirmer
# Date 1095884964 -7200
# Node ID 4481ada46cbb25ab970fc10289b67091b68a94fe
# Parent  d14a6e421a6591d2dcaece5a1fb4a9ad680fb933
bug-fix

diff -r d14a6e421a65 -r 4481ada46cbb src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sun Sep 19 16:51:10 2004 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Sep 22 22:29:24 2004 +0200
@@ -800,21 +800,18 @@
 
 
 fun prove_split_simp sg T prop =
-  (case get_splits sg (rec_id T) of
-     Some (all_thm,_,_,_) 
-     => let
-	   val {sel_upd={simpset,...},extsplit,...} = RecordsData.get_sg sg;
-           val extsplits = 
-                 foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms) 
+  let 
+    val {sel_upd={simpset,...},extsplit,...} = RecordsData.get_sg sg;
+    val extsplits = 
+            foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms) 
                     ([],dest_recTs T);
-           val thms = all_thm::(case extsplits of [thm] => [] | _ => extsplits);
-                                     (* [thm] is the same as all_thm *)
-        in (quick_and_dirty_prove sg [] prop 
-            (fn _ => (simp_tac (simpset addsimps thms) 1)))
-        end
-   | _ => error "RecordPackage.prove_split_simp:code should never been reached")
-
-
+    val thms = (case get_splits sg (rec_id T) of
+                   Some (all_thm,_,_,_) => 
+                     all_thm::(case extsplits of [thm] => [] | _ => extsplits)
+                              (* [thm] is the same as all_thm *)
+                 | None => extsplits)                                
+  in (quick_and_dirty_prove sg [] prop (fn _ => (simp_tac (simpset addsimps thms) 1)))
+  end;
 
 local