src/HOL/Tools/function_package/fundef_lib.ML

--- a/src/HOL/Tools/function_package/fundef_lib.ML	Wed Oct 04 01:43:57 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Wed Oct 04 11:18:39 2006 +0200
@@ -127,3 +127,8 @@
 fun frees_in_term ctxt t =
     rev (fold_aterms (fn  Free (v as (x, _)) =>
                           if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t [])
+
+
+fun plural sg pl [] = sys_error "plural"
+  | plural sg pl [x] = sg
+  | plural sg pl (x::y::ys) = pl