# HG changeset patch
# User wenzelm
# Date 779551326 -7200
# Node ID 11098f505bfeb8afec03bf0d292093fb51e44f62
# Parent  ede55dd46f9dc129d9eba4f4ba40e156f74a2f42
now uses Sign.const_type;

diff -r ede55dd46f9d -r 11098f505bfe src/CCL/CCL.ML
--- a/src/CCL/CCL.ML	Wed Sep 14 14:49:56 1994 +0200
+++ b/src/CCL/CCL.ML	Wed Sep 14 16:02:06 1994 +0200
@@ -88,7 +88,7 @@
          | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
          | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s);
            val sg = sign_of thy;
-           val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),sy) of
+           val T = case Sign.const_type sg sy of
   		            None => error(sy^" not declared") | Some(T) => T;
            val arity = length (fst (strip_type T));
        in sy ^ (arg_str arity name "") end;
diff -r ede55dd46f9d -r 11098f505bfe src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Wed Sep 14 14:49:56 1994 +0200
+++ b/src/FOLP/simp.ML	Wed Sep 14 16:02:06 1994 +0200
@@ -590,7 +590,7 @@
 
 fun mk_cong_thy thy f =
 let val sg = sign_of thy;
-    val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
+    val T = case Sign.const_type sg f of
 		None => error(f^" not declared") | Some(T) => T;
     val T' = incr_tvar 9 T;
 in mk_cong_type sg (Const(f,T'),T') end;
@@ -602,7 +602,7 @@
     val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
     fun readfT(f,s) =
 	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
-	    val t = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
+	    val t = case Sign.const_type sg f of
 		      Some(_) => Const(f,T) | None => Free(f,T)
 	in (t,T) end
 in flat o map (mk_cong_type sg o readfT) end;
diff -r ede55dd46f9d -r 11098f505bfe src/Provers/simp.ML
--- a/src/Provers/simp.ML	Wed Sep 14 14:49:56 1994 +0200
+++ b/src/Provers/simp.ML	Wed Sep 14 16:02:06 1994 +0200
@@ -617,7 +617,7 @@
 
 fun mk_cong_thy thy f =
 let val sg = sign_of thy;
-    val T = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
+    val T = case Sign.const_type sg f of
 		None => error(f^" not declared") | Some(T) => T;
     val T' = incr_tvar 9 T;
 in mk_cong_type sg (Const(f,T'),T') end;
@@ -629,7 +629,7 @@
     val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
     fun readfT(f,s) =
 	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
-	    val t = case Sign.Symtab.lookup(#const_tab(Sign.rep_sg sg),f) of
+	    val t = case Sign.const_type sg f of
 		      Some(_) => Const(f,T) | None => Free(f,T)
 	in (t,T) end
 in flat o map (mk_cong_type sg o readfT) end;