# HG changeset patch
# User wenzelm
# Date 877108076 -7200
# Node ID 3553fcfa2c7e8bbc9b6d3bc8207bd1bf119daa61
# Parent  787d2659ce4ab8ecdd8b5415546a061281e437f8
adapted to qualified names;

diff -r 787d2659ce4a -r 3553fcfa2c7e src/CTT/CTT.ML
--- 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!*) 
diff -r 787d2659ce4a -r 3553fcfa2c7e src/CTT/ROOT.ML
--- 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";