# HG changeset patch
# User traytel
# Date 1346687799 -7200
# Node ID 3caaa80f53a4a6eb7bfe2d774eea1227f58dc69e
# Parent  ce2ef34eb82822ca61c78d1a076030d3f47f2682
generalized signature

diff -r ce2ef34eb828 -r 3caaa80f53a4 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Mon Sep 03 17:55:42 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Mon Sep 03 17:56:39 2012 +0200
@@ -71,7 +71,7 @@
   val wit_thmss_of_bnf: BNF -> thm list list
 
   val mk_witness: int list * term -> thm list -> nonemptiness_witness
-  val minimize_wits: (''a list * term) list -> (''a list * term) list
+  val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
   val wits_of_bnf: BNF -> nonemptiness_witness list
 
   datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
@@ -447,7 +447,7 @@
 fun minimize_wits wits =
  let
    fun minimize done [] = done
-     | minimize done ((I, wit : term) :: todo) =
+     | minimize done ((I, wit) :: todo) =
        if exists (fn (J, _) => subset (op =) (J, I)) (done @ todo)
        then minimize done todo
        else minimize ((I, wit) :: done) todo;