# HG changeset patch
# User wenzelm
# Date 1192122617 -7200
# Node ID 821628d165524ffd59d7942b425028ff21f0100e
# Parent  592a5d8700a7e2988947343fad3e79e98c3fbf4c
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);

diff -r 592a5d8700a7 -r 821628d16552 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Oct 11 18:58:34 2007 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 11 19:10:17 2007 +0200
@@ -2030,7 +2030,7 @@
 				 names'
 				 (thy1,th)
 	    val _ = ImportRecorder.add_specification names' th
-	    val res' = Drule.unvarify res
+	    val res' = Thm.unvarify res
 	    val hth = HOLThm(rens,res')
 	    val rew = rewrite_hol4_term (concl_of res') thy'
 	    val th  = equal_elim rew res'
diff -r 592a5d8700a7 -r 821628d16552 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Thu Oct 11 18:58:34 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Oct 11 19:10:17 2007 +0200
@@ -411,7 +411,7 @@
       (#case_rewrites o DatatypePackage.the_datatype thy) tyco;
     val thms as hd_thm :: _ = raw_thms
       |> Conjunction.intr_balanced
-      |> Drule.unvarify
+      |> Thm.unvarify
       |> Conjunction.elim_balanced (length raw_thms)
       |> map Simpdata.mk_meta_eq
       |> map Drule.zero_var_indexes
diff -r 592a5d8700a7 -r 821628d16552 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Thu Oct 11 18:58:34 2007 +0200
+++ b/src/Pure/conjunction.ML	Thu Oct 11 19:10:17 2007 +0200
@@ -69,7 +69,7 @@
 val ABC = read_prop "A ==> B ==> C";
 val A_B = read_prop "A && B";
 
-val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
+val conjunction_def = Thm.unvarify ProtoPure.conjunction_def;
 
 fun conjunctionD which =
   Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
diff -r 592a5d8700a7 -r 821628d16552 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Thu Oct 11 18:58:34 2007 +0200
+++ b/src/Tools/code/code_package.ML	Thu Oct 11 19:10:17 2007 +0200
@@ -157,7 +157,7 @@
 
 fun mk_codeprops thy all_cs sel_cs =
   let
-    fun select (thmref, thm) = case try (Drule.unvarify o Drule.zero_var_indexes) thm
+    fun select (thmref, thm) = case try (Thm.unvarify o Drule.zero_var_indexes) thm
      of NONE => NONE
       | SOME thm => let
           val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm;