diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Lift.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -4,11 +4,11 @@
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-header {* Lifting types of class term to flat pcpo's *}
+header {* Lifting types of class type to flat pcpo's *}
 
 theory Lift = Cprod3:
 
-defaultsort "term"
+defaultsort type
 
 
 typedef 'a lift = "UNIV :: 'a option set" ..
@@ -19,12 +19,12 @@
   Def :: "'a => 'a lift"
   "Def x == Abs_lift (Some x)"
 
-instance lift :: ("term") sq_ord ..
+instance lift :: (type) sq_ord ..
 
 defs (overloaded)
   less_lift_def: "x << y == (x=y | x=Undef)"
 
-instance lift :: ("term") po
+instance lift :: (type) po
 proof
   fix x y z :: "'a lift"
   show "x << x" by (unfold less_lift_def) blast
@@ -111,7 +111,7 @@
   apply (blast intro: lub_finch1)
   done
 
-instance lift :: ("term") pcpo
+instance lift :: (type) pcpo
   apply intro_classes
    apply (erule cpo_lift)
   apply (rule least_lift)
@@ -153,7 +153,7 @@
 consts
  flift1      :: "('a => 'b::pcpo) => ('a lift -> 'b)"
  flift2      :: "('a => 'b)       => ('a lift -> 'b lift)"
- liftpair    ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
+ liftpair    ::"'a::type lift * 'b::type lift => ('a * 'b) lift"
 
 defs
  flift1_def:
@@ -219,7 +219,7 @@
 
 subsection {* Lift is flat *}
 
-instance lift :: ("term") flat
+instance lift :: (type) flat
 proof
   show "ALL x y::'a lift. x << y --> x = UU | x = y"
     by (simp add: less_lift)