TFL/tfl.ML

 
 
 (*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)
   | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
   | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);