# HG changeset patch
# User wenzelm
# Date 1177581612 -7200
# Node ID 4b77a43f7f587a0b4fa3d6fb4bd3ea96b7aa448d
# Parent  34c316d7b630c8c96c76b6de972d0445ae78559a
mk_const_def: Sign.intern_term (legacy);

diff -r 34c316d7b630 -r 4b77a43f7f58 TFL/tfl.ML
--- a/TFL/tfl.ML	Thu Apr 26 12:00:05 2007 +0200
+++ b/TFL/tfl.ML	Thu Apr 26 12:00:12 2007 +0200
@@ -368,7 +368,7 @@
 (*For Isabelle, the lhs of a definition must be a constant.*)
 fun mk_const_def sign (c, Ty, rhs) =
   singleton (ProofContext.infer_types (ProofContext.init sign))
-    (Const("==",dummyT) $ Const(Sign.full_name sign c,Ty) $ rhs);
+    (Sign.intern_term sign (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)