src/HOL/Tools/inductive_codegen.ML

--- a/src/HOL/Tools/inductive_codegen.ML	Sun Feb 12 20:32:59 2006 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Sun Feb 12 21:34:18 2006 +0100
@@ -20,7 +20,7 @@
 
 fun merge_rules tabs =
   Symtab.join (fn _ => fn (ths, ths') =>
-    SOME (gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths')) tabs;
+    gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths') tabs;
 
 structure CodegenData = TheoryDataFun
 (struct