# HG changeset patch
# User wenzelm
# Date 1144922456 -7200
# Node ID 2d26166aca27ec36ca6a37fcefbd89e93c2f03e8
# Parent  03b01c9314fc1bb8730e757f27ff8b1721854aa4
ignore sorts of consts declarations;

diff -r 03b01c9314fc -r 2d26166aca27 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Thu Apr 13 12:00:55 2006 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Thu Apr 13 12:00:56 2006 +0200
@@ -75,7 +75,7 @@
       (t as Const (s, T)) = if T = dummyT then (case Sign.const_type sg s of
           NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
         | SOME T => 
-            let val T' = Logic.incr_tvar (maxidx + 1) T
+            let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
             in (Const (s, T'), T', vTs,
               Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
             end)
diff -r 03b01c9314fc -r 2d26166aca27 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Apr 13 12:00:55 2006 +0200
+++ b/src/Pure/codegen.ML	Thu Apr 13 12:00:56 2006 +0200
@@ -375,7 +375,7 @@
                 NONE => T
               | SOME ty =>
                   let val U = prep_type thy ty
-                  in if Sign.typ_instance thy (U, T) then U
+                  in if Type.raw_instance (U, T) then U
                     else error ("Illegal type constraint for constant " ^ cname)
                   end)
          in