# HG changeset patch
# User krauss
# Date 1164371962 -3600
# Node ID 7e72185e4b242a43df37a8b082b10de7d20b7724
# Parent  6c5755ad9caeaac042d34453455e4064a8460b31
exported mk_base_funs for use by size-change tools

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