# HG changeset patch
# User wenzelm
# Date 1324130951 -3600
# Node ID 566c34b64f7068326024172fd1dec94163e7ad87
# Parent  6fe61da4c4677529e0f3505095858c98d7437d82
eliminated Drule.export_without_context which is not really required here;

diff -r 6fe61da4c467 -r 566c34b64f70 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Dec 17 13:08:03 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Dec 17 15:09:11 2011 +0100
@@ -252,12 +252,8 @@
       let
         val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
         val rep_const = cterm_of thy (Const (#Rep_name (#1 typedef), T --> Univ_elT));
-        val cong' =
-          Drule.export_without_context
-            (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
-        val dist =
-          Drule.export_without_context
-            (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
+        val cong' = cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong;
+        val dist = cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma;
         val (thy', defs', eqns', _) =
           fold (make_constr_def typedef T (length constrs))
             (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
@@ -543,7 +539,7 @@
               let
                 val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ =>
                   EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
-              in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: prove ts end;
+              in dist_thm :: Drule.zero_var_indexes (dist_thm RS not_sym) :: prove ts end;
       in prove end;
 
     val distinct_thms =