# HG changeset patch
# User blanchet
# Date 1367496296 -7200
# Node ID 75655198442e036b25fb90df9418a5c94beaf9d6
# Parent  09d24ea3f140bb593ee3719590e649e15dbd4ed5
export one more function

diff -r 09d24ea3f140 -r 75655198442e src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 12:35:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 14:04:56 2013 +0200
@@ -21,6 +21,7 @@
 
   val fp_sugar_of: local_theory -> string -> fp_sugar option
 
+  val exists_subtype_in: typ list -> typ -> bool
   val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c
   val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
 
@@ -143,7 +144,7 @@
     let val (xs1, xs2, xs3, xs4) = split_list4 xs;
     in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
 
-fun exists_subtype_in Ts = exists_subtype (member (op =) Ts);
+val exists_subtype_in = Term.exists_subtype o member (op =);
 
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);