src/CTT/CTT.ML
changeset 3929 3553fcfa2c7e
parent 3837 d7f033c74b38
child 4440 9ed4098074bc
     1.1 --- a/src/CTT/CTT.ML	Fri Oct 17 18:19:14 1997 +0200
     1.2 +++ b/src/CTT/CTT.ML	Fri Oct 17 19:07:56 1997 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  
     1.5  (** Tactics for type checking **)
     1.6  
     1.7 -fun is_rigid_elem (Const("Elem",_) $ a $ _) = not (is_Var (head_of a))
     1.8 +fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not (is_Var (head_of a))
     1.9    | is_rigid_elem _ = false;
    1.10  
    1.11  (*Try solving a:A by assumption provided a is rigid!*)