adapted to qualified names;

--- a/src/CTT/CTT.ML	Fri Oct 17 18:19:14 1997 +0200
+++ b/src/CTT/CTT.ML	Fri Oct 17 19:07:56 1997 +0200
@@ -55,7 +55,7 @@
 
 (** Tactics for type checking **)
 
-fun is_rigid_elem (Const("Elem",_) $ a $ _) = not (is_Var (head_of a))
+fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not (is_Var (head_of a))
   | is_rigid_elem _ = false;
 
 (*Try solving a:A by assumption provided a is rigid!*) 

--- a/src/CTT/ROOT.ML	Fri Oct 17 18:19:14 1997 +0200
+++ b/src/CTT/ROOT.ML	Fri Oct 17 19:07:56 1997 +0200
@@ -10,6 +10,8 @@
 val banner = "Constructive Type Theory";
 writeln banner;
 
+reset global_names;
+
 print_depth 1;  
 
 use_thy "CTT";