src/FOLP/simp.ML
changeset 611 11098f505bfe
parent 231 cb6a24451544
child 1459 d12da312eff4
     1.1 --- a/src/FOLP/simp.ML	Wed Sep 14 14:49:56 1994 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed Sep 14 16:02:06 1994 +0200
     1.3 @@ -590,7 +590,7 @@
     1.4  
     1.5  fun mk_cong_thy thy f =
     1.6  let val sg = sign_of thy;
     1.7 -    val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
     1.8 +    val T = case Sign.const_type sg f of
     1.9  		None => error(f^" not declared") | Some(T) => T;
    1.10      val T' = incr_tvar 9 T;
    1.11  in mk_cong_type sg (Const(f,T'),T') end;
    1.12 @@ -602,7 +602,7 @@
    1.13      val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
    1.14      fun readfT(f,s) =
    1.15  	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
    1.16 -	    val t = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
    1.17 +	    val t = case Sign.const_type sg f of
    1.18  		      Some(_) => Const(f,T) | None => Free(f,T)
    1.19  	in (t,T) end
    1.20  in flat o map (mk_cong_type sg o readfT) end;