src/HOLCF/Tools/domain/domain_theorems.ML

--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Jul 21 23:25:00 2007 +0200
@@ -195,7 +195,7 @@
       val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
     in Library.foldr mk_ex (vns, conj) end;
 
-  val conj_assoc = thm "conj_assoc";
+  val conj_assoc = @{thm conj_assoc};
   val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
   val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
   val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
@@ -333,7 +333,7 @@
 end;
 
 local
-  val rev_contrapos = thm "rev_contrapos";
+  val rev_contrapos = @{thm rev_contrapos};
   fun con_strict (con, args) = 
     let
       fun one_strict vn =
@@ -441,7 +441,7 @@
 end;
 
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
-val rev_contrapos = thm "rev_contrapos";
+val rev_contrapos = @{thm rev_contrapos};
 
 val distincts_le =
   let