diff -r 944f9bf26d2d -r 03ad378ed5f0 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Apr 03 16:34:52 2008 +0200
@@ -37,7 +37,6 @@
       psimps : thm list, 
       trsimps : thm list option, 
 
-      subset_pinducts : thm list, 
       simple_pinducts : thm list, 
       cases : thm,
       termination : thm,
@@ -51,7 +50,8 @@
       defname : string,
 
       (* contains no logical entities: invariant under morphisms *)
-      add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+      add_simps : (string -> string) -> string -> Attrib.src list -> thm list 
+                  -> local_theory -> thm list * local_theory,
       case_names : string list,
 
       fs : term list,
@@ -179,9 +179,7 @@
     let
       fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
       val (qs, imp) = open_all_all geq
-
-      val gs = Logic.strip_imp_prems imp
-      val eq = Logic.strip_imp_concl imp
+      val (gs, eq) = Logic.strip_horn imp
 
       val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
           handle TERM _ => error (input_error "Not an equation")