# HG changeset patch
# User wenzelm
# Date 1442148154 -7200
# Node ID c94c65f35d01c1198f1d5c3dce0cb24df38ec4cd
# Parent  61908914d1913b328a818debe442c99bb889e6f9
tuned;

diff -r 61908914d191 -r c94c65f35d01 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Sep 10 12:52:24 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Sun Sep 13 14:42:34 2015 +0200
@@ -473,8 +473,7 @@
         (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
            fold_rev lambda params (HOLogic.Collect_const U $
              HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
-           (cnames_syn ~~ cs_info ~~ preds))
-      ||> Proof_Context.restore_naming lthy1;
+           (cnames_syn ~~ cs_info ~~ preds));
 
     (* prove theorems for converting predicate to set notation *)
     val lthy3 = fold