src/HOLCF/Fix.ML

         (etac spec 1),
         (Asm_simp_tac 1)
         ]);
 
 
-val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
+bind_thm ("adm_flat", flat_imp_chain_finite RS adm_chain_finite);
 (* is_flat(?x::?'a) ==> adm(?P::?'a => bool) *)
 
 qed_goalw "flat_void" Fix.thy [is_flat_def] "is_flat(UU::void)"
  (fn prems =>
         [

         (rtac allI 1),
         (dtac spec 1),
         (etac spec 1)
         ]);
 
-val adm_all2 = (allI RS adm_all);
+bind_thm ("adm_all2", allI RS adm_all);
 
 qed_goal "adm_subst"  Fix.thy  
         "[|cont t; adm P|] ==> adm(%x. P (t x))"
  (fn prems =>
         [