diff -r d53f76357f41 -r 617fdb08abe9 src/HOL/Tools/function_package/termination.ML
--- a/src/HOL/Tools/function_package/termination.ML	Wed Nov 08 21:45:15 2006 +0100
+++ b/src/HOL/Tools/function_package/termination.ML	Wed Nov 08 22:24:54 2006 +0100
@@ -9,8 +9,8 @@
 
 signature FUNDEF_TERMINATION =
 sig
-  val mk_total_termination_goal : FundefCommon.result_with_names -> term
-  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
+  val mk_total_termination_goal : term -> term -> term
+(*  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*)
 end
 
 structure FundefTermination : FUNDEF_TERMINATION =
@@ -21,7 +21,7 @@
 open FundefCommon
 open FundefAbbrev
      
-fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
+fun mk_total_termination_goal f R =
     let
       val domT = domain_type (fastype_of f)
       val x = Free ("x", domT)
@@ -29,6 +29,7 @@
       mk_forall x (Trueprop (mk_acc domT R $ x))
     end
     
+(*
 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
     let
       val domT = domain_type (fastype_of f)
@@ -55,7 +56,7 @@
     in
       (subs, dcl)
     end
-
+*)
 end