Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/tfl.ML
changeset 22797 4b77a43f7f58
parent 22728 ecbbdf50df2f 
--- 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)
isabelle