src/FOLP/simp.ML
changeset 16876 f57b38cced32
parent 16800 90eff1b52428
child 16931 e41d8e319dfd
     1.1 --- a/src/FOLP/simp.ML	Tue Jul 19 17:21:46 2005 +0200
     1.2 +++ b/src/FOLP/simp.ML	Tue Jul 19 17:21:47 2005 +0200
     1.3 @@ -593,7 +593,7 @@
     1.4  let val sg = sign_of thy;
     1.5      val T = case Sign.const_type sg f of
     1.6                  NONE => error(f^" not declared") | SOME(T) => T;
     1.7 -    val T' = incr_tvar 9 T;
     1.8 +    val T' = Logic.incr_tvar 9 T;
     1.9  in mk_cong_type sg (Const(f,T'),T') end;
    1.10  
    1.11  fun mk_congs thy = List.concat o map (mk_cong_thy thy);
    1.12 @@ -602,7 +602,7 @@
    1.13  let val sg = sign_of thy;
    1.14      val S0 = Sign.defaultS sg;
    1.15      fun readfT(f,s) =
    1.16 -        let val T = incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s);
    1.17 +        let val T = Logic.incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s);
    1.18              val t = case Sign.const_type sg f of
    1.19                        SOME(_) => Const(f,T) | NONE => Free(f,T)
    1.20          in (t,T) end