now uses Sign.const_type;
authorwenzelm
Wed Sep 14 16:02:06 1994 +0200 (1994-09-14)
changeset 61111098f505bfe
parent 610 ede55dd46f9d
child 612 1ebe4d36dedc
now uses Sign.const_type;
src/CCL/CCL.ML
src/FOLP/simp.ML
src/Provers/simp.ML
     1.1 --- a/src/CCL/CCL.ML	Wed Sep 14 14:49:56 1994 +0200
     1.2 +++ b/src/CCL/CCL.ML	Wed Sep 14 16:02:06 1994 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4           | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
     1.5           | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s);
     1.6             val sg = sign_of thy;
     1.7 -           val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),sy) of
     1.8 +           val T = case Sign.const_type sg sy of
     1.9    		            None => error(sy^" not declared") | Some(T) => T;
    1.10             val arity = length (fst (strip_type T));
    1.11         in sy ^ (arg_str arity name "") end;
     2.1 --- a/src/FOLP/simp.ML	Wed Sep 14 14:49:56 1994 +0200
     2.2 +++ b/src/FOLP/simp.ML	Wed Sep 14 16:02:06 1994 +0200
     2.3 @@ -590,7 +590,7 @@
     2.4  
     2.5  fun mk_cong_thy thy f =
     2.6  let val sg = sign_of thy;
     2.7 -    val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
     2.8 +    val T = case Sign.const_type sg f of
     2.9  		None => error(f^" not declared") | Some(T) => T;
    2.10      val T' = incr_tvar 9 T;
    2.11  in mk_cong_type sg (Const(f,T'),T') end;
    2.12 @@ -602,7 +602,7 @@
    2.13      val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
    2.14      fun readfT(f,s) =
    2.15  	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
    2.16 -	    val t = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
    2.17 +	    val t = case Sign.const_type sg f of
    2.18  		      Some(_) => Const(f,T) | None => Free(f,T)
    2.19  	in (t,T) end
    2.20  in flat o map (mk_cong_type sg o readfT) end;
     3.1 --- a/src/Provers/simp.ML	Wed Sep 14 14:49:56 1994 +0200
     3.2 +++ b/src/Provers/simp.ML	Wed Sep 14 16:02:06 1994 +0200
     3.3 @@ -617,7 +617,7 @@
     3.4  
     3.5  fun mk_cong_thy thy f =
     3.6  let val sg = sign_of thy;
     3.7 -    val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
     3.8 +    val T = case Sign.const_type sg f of
     3.9  		None => error(f^" not declared") | Some(T) => T;
    3.10      val T' = incr_tvar 9 T;
    3.11  in mk_cong_type sg (Const(f,T'),T') end;
    3.12 @@ -629,7 +629,7 @@
    3.13      val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
    3.14      fun readfT(f,s) =
    3.15  	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
    3.16 -	    val t = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
    3.17 +	    val t = case Sign.const_type sg f of
    3.18  		      Some(_) => Const(f,T) | None => Free(f,T)
    3.19  	in (t,T) end
    3.20  in flat o map (mk_cong_type sg o readfT) end;