# HG changeset patch
# User haftmann
# Date 1207144722 -7200
# Node ID 6cd53b7ef55ce36284da48c4ed47d38c69f123ba
# Parent  3db6a46d8460ad128ab131bef2fc7bbe923dd697
subst_alias

diff -r 3db6a46d8460 -r 6cd53b7ef55c src/Pure/Isar/code_unit.ML
--- 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