src/FOLP/simp.ML
changeset 24707 dfeb98f84e93
parent 22675 acf10be7dcca
child 26928 ca87aff1ad2d
     1.1 --- a/src/FOLP/simp.ML	Tue Sep 25 13:28:35 2007 +0200
     1.2 +++ b/src/FOLP/simp.ML	Tue Sep 25 13:28:37 2007 +0200
     1.3 @@ -594,7 +594,7 @@
     1.4  let
     1.5    fun readfT(f,s) =
     1.6      let
     1.7 -      val T = Logic.incr_tvar 9 (Sign.read_typ thy s);
     1.8 +      val T = Logic.incr_tvar 9 (Syntax.read_typ_global thy s);
     1.9        val t = case Sign.const_type thy f of
    1.10                    SOME(_) => Const(f,T) | NONE => Free(f,T)
    1.11      in (t,T) end