src/HOL/Tools/inductive_codegen.ML
changeset 19025 596fb1eb7856
parent 18964 67f572e03236
child 19046 bc5c6c9b114e
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun Feb 12 20:32:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sun Feb 12 21:34:18 2006 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  fun merge_rules tabs =
     1.6    Symtab.join (fn _ => fn (ths, ths') =>
     1.7 -    SOME (gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths')) tabs;
     1.8 +    gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths') tabs;
     1.9  
    1.10  structure CodegenData = TheoryDataFun
    1.11  (struct