# HG changeset patch
# User wenzelm
# Date 877337302 -7200
# Node ID 52c14fe8f16b71c4f6aace2cea465af56506fd4c
# Parent  a9c8960e4da6ea202fd6e93fd331adeed4372f1e
adapted to qualified names;

diff -r a9c8960e4da6 -r 52c14fe8f16b src/CCL/CCL.ML
--- a/src/CCL/CCL.ML	Mon Oct 20 10:39:26 1997 +0200
+++ b/src/CCL/CCL.ML	Mon Oct 20 10:48:22 1997 +0200
@@ -87,7 +87,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.const_type sg sy of
+           val T = case Sign.const_type sg (Sign.intern_const (sign_of thy) 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 a9c8960e4da6 -r 52c14fe8f16b src/CCL/Set.thy
--- a/src/CCL/Set.thy	Mon Oct 20 10:39:26 1997 +0200
+++ b/src/CCL/Set.thy	Mon Oct 20 10:48:22 1997 +0200
@@ -7,6 +7,8 @@
 
 Set = FOL +
 
+global
+
 types
   'a set
 
@@ -28,6 +30,7 @@
   empty         :: "'a set"                             ("{}")
   "oo"          :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50) (*composition*)
 
+syntax
   "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
 
   (* Big Intersection / Union *)
@@ -48,6 +51,7 @@
   "ALL x:A. P"  == "Ball(A, %x. P)"
   "EX x:A. P"   == "Bex(A, %x. P)"
 
+local
 
 rules
   mem_Collect_iff       "(a : {x. P(x)}) <-> P(a)"