src/ZF/OrderType.ML
changeset 803 4c8333ab3eae
parent 788 8acbe6f3de2b
child 807 3abd026e68a4
--- a/src/ZF/OrderType.ML	Fri Dec 16 17:46:02 1994 +0100
+++ b/src/ZF/OrderType.ML	Fri Dec 16 18:07:12 1994 +0100
@@ -94,10 +94,9 @@
 by (assume_tac 1);
 qed "converse_ordermap_mono";
 
-val ordermap_surj = 
-    (ordermap_type RS surj_image) |>
-    rewrite_rule [symmetric ordertype_def] |> 
-    standard;
+bind_thm ("ordermap_surj", 
+	  rewrite_rule [symmetric ordertype_def] 
+	      (ordermap_type RS surj_image));
 
 goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
     "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";