src/HOL/Real/PReal.ML

     "(z1::preal) + (z2 + z3) = z2 + (z1 + z3)"
  (fn _ => [rtac (preal_add_commute RS trans) 1, rtac (preal_add_assoc RS trans) 1,
            rtac (preal_add_commute RS arg_cong) 1]);
 
 (* Positive Reals addition is an AC operator *)
-val preal_add_ac = [preal_add_assoc, preal_add_commute, preal_add_left_commute];
+bind_thms ("preal_add_ac", [preal_add_assoc, preal_add_commute, preal_add_left_commute]);
 
   (*** Properties of multiplication ***)
 
 (** Proofs essentially same as for addition **)
 

  (fn _ => [rtac (preal_mult_commute RS trans) 1, 
            rtac (preal_mult_assoc RS trans) 1,
            rtac (preal_mult_commute RS arg_cong) 1]);
 
 (* Positive Reals multiplication is an AC operator *)
-val preal_mult_ac = [preal_mult_assoc, 
+bind_thms ("preal_mult_ac", [preal_mult_assoc, 
                      preal_mult_commute, 
-                     preal_mult_left_commute];
+                     preal_mult_left_commute]);
 
 (* Positive Real 1 is the multiplicative identity element *) 
 (* long *)
 Goalw [preal_of_prat_def,preal_mult_def] 
       "(preal_of_prat (prat_of_pnat (Abs_pnat 1))) * z = z";

 Goalw [preal_le_def,psubset_def,preal_less_def] 
                      "z<=w ==> ~(w<(z::preal))";
 by (auto_tac  (claset() addDs [equalityI],simpset()));
 qed "preal_leD";
 
-val preal_leE = make_elim preal_leD;
+bind_thm ("preal_leE", make_elim preal_leD);
 
 Goalw [preal_le_def,psubset_def,preal_less_def]
                    "~ z <= w ==> w<(z::preal)";
 by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
 by (auto_tac  (claset(),simpset() addsimps [preal_less_def,psubset_def]));