Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
subst_alias
authorhaftmann
Wed, 02 Apr 2008 15:58:42 +0200
changeset 26519 6cd53b7ef55c
parent 26518 3db6a46d8460
child 26520 9e7b7c478cb1
subst_alias
src/Pure/Isar/code_unit.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/code_unit.ML	Wed Apr 02 15:58:41 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML	Wed Apr 02 15:58:42 2008 +0200
@@ -248,11 +248,13 @@
  of SOME c_ty => c_ty
   | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t);
 
-fun check_const thy = subst_alias thy o AxClass.unoverload_const thy o check_bare_const thy;
+fun check_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
+  o check_bare_const thy;
 
 fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
 
-fun read_const thy = subst_alias thy o AxClass.unoverload_const thy o read_bare_const thy;
+fun read_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
+  o read_bare_const thy;
 
 local
isabelle