diff -r 6c5755ad9cae -r 7e72185e4b24 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Nov 24 13:24:30 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Nov 24 13:39:22 2006 +0100
@@ -8,6 +8,11 @@
 signature LEXICOGRAPHIC_ORDER =
 sig
   val lexicographic_order : Proof.context -> Method.method
+
+  (* exported for use by size-change termination prototype.
+     FIXME: provide a common interface later *)
+  val mk_base_funs : typ -> term list
+
   val setup: theory -> theory
 end