1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Oct 11 18:58:34 2007 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 11 19:10:17 2007 +0200
     1.3 @@ -2030,7 +2030,7 @@
     1.4  				 names'
     1.5  				 (thy1,th)
     1.6  	    val _ = ImportRecorder.add_specification names' th
     1.7 -	    val res' = Drule.unvarify res
     1.8 +	    val res' = Thm.unvarify res
     1.9  	    val hth = HOLThm(rens,res')
    1.10  	    val rew = rewrite_hol4_term (concl_of res') thy'
    1.11  	    val th  = equal_elim rew res'

     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Oct 11 18:58:34 2007 +0200
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Oct 11 19:10:17 2007 +0200
     2.3 @@ -411,7 +411,7 @@
     2.4        (#case_rewrites o DatatypePackage.the_datatype thy) tyco;
     2.5      val thms as hd_thm :: _ = raw_thms
     2.6        |> Conjunction.intr_balanced
     2.7 -      |> Drule.unvarify
     2.8 +      |> Thm.unvarify
     2.9        |> Conjunction.elim_balanced (length raw_thms)
    2.10        |> map Simpdata.mk_meta_eq
    2.11        |> map Drule.zero_var_indexes

     3.1 --- a/src/Pure/conjunction.ML	Thu Oct 11 18:58:34 2007 +0200
     3.2 +++ b/src/Pure/conjunction.ML	Thu Oct 11 19:10:17 2007 +0200
     3.3 @@ -69,7 +69,7 @@
     3.4  val ABC = read_prop "A ==> B ==> C";
     3.5  val A_B = read_prop "A && B";
     3.6  
     3.7 -val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
     3.8 +val conjunction_def = Thm.unvarify ProtoPure.conjunction_def;
     3.9  
    3.10  fun conjunctionD which =
    3.11    Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP

     4.1 --- a/src/Tools/code/code_package.ML	Thu Oct 11 18:58:34 2007 +0200
     4.2 +++ b/src/Tools/code/code_package.ML	Thu Oct 11 19:10:17 2007 +0200
     4.3 @@ -157,7 +157,7 @@
     4.4  
     4.5  fun mk_codeprops thy all_cs sel_cs =
     4.6    let
     4.7 -    fun select (thmref, thm) = case try (Drule.unvarify o Drule.zero_var_indexes) thm
     4.8 +    fun select (thmref, thm) = case try (Thm.unvarify o Drule.zero_var_indexes) thm
     4.9       of NONE => NONE
    4.10        | SOME thm => let
    4.11            val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm;