src/HOLCF/Tr1.ML

--- a/src/HOLCF/Tr1.ML	Thu Nov 28 15:56:04 1996 +0100
+++ b/src/HOLCF/Tr1.ML	Fri Nov 29 12:15:33 1996 +0100
@@ -123,7 +123,7 @@
 (* type tr is flat                                                          *) 
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "flat_tr" Tr1.thy [is_flat_def] "is_flat(TT)"
+qed_goalw "flat_tr" Tr1.thy [flat_def] "flat TT"
  (fn prems =>
         [
         (rtac allI 1),