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