diff -r 1b1b46adc9b3 -r dbce3dce821a src/HOLCF/One.ML
--- a/src/HOLCF/One.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/One.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/one.thy
+(*  Title:      HOLCF/One.ML
     ID:         $Id$
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
@@ -15,7 +15,7 @@
 qed_goalw "Exh_one" One.thy [one_def] "z=UU | z = one"
  (fn prems =>
         [
-        (res_inst_tac [("p","rep_one`z")] liftE1 1),
+        (res_inst_tac [("p","rep_one`z")] upE1 1),
         (rtac disjI1 1),
         (rtac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict )
                 RS conjunct2 RS subst) 1),
@@ -46,7 +46,7 @@
  (fn prems =>
         [
         (rtac classical3 1),
-        (rtac less_lift4b 1),
+        (rtac less_up4b 1),
         (rtac (rep_one_iso RS subst) 1),
         (rtac (rep_one_iso RS subst) 1),
         (rtac monofun_cfun_arg 1),
@@ -68,7 +68,7 @@
 (* one is flat                                                              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "flat_one" One.thy [is_flat_def] "is_flat(one)"
+qed_goalw "flat_one" One.thy [flat_def] "flat one"
  (fn prems =>
         [
         (rtac allI 1),