src/Pure/logic.ML
changeset 19391 4812d28c90a6
parent 19125 59b26248547b
child 19406 410b9d9bf9a1
     1.1 --- a/src/Pure/logic.ML	Sun Apr 09 19:41:30 2006 +0200
     1.2 +++ b/src/Pure/logic.ML	Mon Apr 10 00:33:49 2006 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4  
     1.5  (** types as terms **)
     1.6  
     1.7 -fun mk_type ty = Const ("TYPE", itselfT ty);
     1.8 +fun mk_type ty = Const ("TYPE", Term.itselfT ty);
     1.9  
    1.10  fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
    1.11    | dest_type t = raise TERM ("dest_type", [t]);
    1.12 @@ -187,7 +187,7 @@
    1.13    handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
    1.14  
    1.15  fun mk_inclass (ty, c) =
    1.16 -  Const (const_of_class c, itselfT ty --> propT) $ mk_type ty;
    1.17 +  Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
    1.18  
    1.19  fun dest_inclass (t as Const (c_class, _) $ ty) =
    1.20        ((dest_type ty, class_of_const c_class)