# HG changeset patch
# User wenzelm
# Date 1268681243 -3600
# Node ID 7adb03f27b28be8cad2a7b147a7cf4c846a2436c
# Parent  fd1bb29f81700959b042310145c2fc2f10345870
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;

diff -r fd1bb29f8170 -r 7adb03f27b28 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Mon Mar 15 18:59:16 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Mon Mar 15 20:27:23 2010 +0100
@@ -203,7 +203,7 @@
  *---------------------------------------------------------------------------*)
 fun define_i strict thy cs ss congs wfs fid R eqs =
   let val {functional,pats} = Prim.mk_functional thy eqs
-      val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional
+      val (thy, def) = Prim.wfrec_definition0 thy fid R functional
       val (lhs, _) = Logic.dest_equals (prop_of def)
       val {induct, rules, tcs} = 
           simplify_defn strict thy cs ss congs wfs fid pats def
@@ -228,8 +228,7 @@
   #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));
 
 fun defer_i thy congs fid eqs =
- let val {rules,R,theory,full_pats_TCs,SV,...} =
-             Prim.lazyR_def thy (Long_Name.base_name fid) congs eqs
+ let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
      val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
      val dummy = writeln "Proving induction theorem ...";
      val induction = Prim.mk_induction theory
diff -r fd1bb29f8170 -r 7adb03f27b28 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Mon Mar 15 18:59:16 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon Mar 15 20:27:23 2010 +0100
@@ -360,9 +360,9 @@
 
 
 (*For Isabelle, the lhs of a definition must be a constant.*)
-fun legacy_const_def sign (c, Ty, rhs) =
+fun const_def sign (c, Ty, rhs) =
   singleton (Syntax.check_terms (ProofContext.init sign))
-    (Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs));
+    (Const("==",dummyT) $ Const(c,Ty) $ rhs);
 
 (*Make all TVars available for instantiation by adding a ? to the front*)
 fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
@@ -376,17 +376,13 @@
       val (wfrec,_) = S.strip_comb rhs
 in
 fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
- let val def_name = if x<>fid then
-                        raise TFL_ERR "wfrec_definition0"
-                                      ("Expected a definition of " ^
-                                             quote fid ^ " but found one of " ^
-                                      quote x)
-                    else x ^ "_def"
+ let val def_name = Long_Name.base_name fid ^ "_def"
      val wfrec_R_M =  map_types poly_tvars
                           (wfrec $ map_types poly_tvars R)
                       $ functional
-     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
+     val def_term = const_def thy (fid, 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 +536,7 @@
      val {lhs,rhs} = S.dest_eq proto_def'
      val (c,args) = S.strip_comb lhs
      val (name,Ty) = dest_atom c
-     val defn = legacy_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
+     val defn = const_def thy (name, Ty, S.list_mk_abs (args,rhs))
      val ([def0], theory) =
        thy
        |> PureThy.add_defs false