# HG changeset patch
# User wenzelm
# Date 1268140686 -3600
# Node ID 6fd0ca1a39668cc527b988a01a69f47ba5ad724d
# Parent  ff2bf50505aba3d34980168eae9eebf8c229c733
renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;

diff -r ff2bf50505ab -r 6fd0ca1a3966 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Tue Mar 09 09:25:23 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Tue Mar 09 14:18:06 2010 +0100
@@ -360,7 +360,7 @@
 
 
 (*For Isabelle, the lhs of a definition must be a constant.*)
-fun mk_const_def sign (c, Ty, rhs) =
+fun legacy_const_def sign (c, Ty, rhs) =
   singleton (Syntax.check_terms (ProofContext.init sign))
     (Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs));
 
@@ -385,7 +385,7 @@
      val wfrec_R_M =  map_types poly_tvars
                           (wfrec $ map_types poly_tvars R)
                       $ functional
-     val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
+     val def_term = legacy_const_def thy (x, Ty, wfrec_R_M)
      val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
  in (thy', def) end;
 end;
@@ -540,7 +540,7 @@
      val {lhs,rhs} = S.dest_eq proto_def'
      val (c,args) = S.strip_comb lhs
      val (name,Ty) = dest_atom c
-     val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
+     val defn = legacy_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
      val ([def0], theory) =
        thy
        |> PureThy.add_defs false