# HG changeset patch
# User wenzelm
# Date 1346444654 -7200
# Node ID 2924a83a4a0b47f6a63f95e4b4af120267af4099
# Parent  01041f7bf9b450a76fa743a74ba8e75d60b598dd
tuned signature;

diff -r 01041f7bf9b4 -r 2924a83a4a0b src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Fri Aug 31 16:35:30 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Aug 31 22:24:14 2012 +0200
@@ -195,7 +195,7 @@
 (* forked proofs *)
 
 val begin_proofs = background_theory (Context.theory_map Thm.begin_proofs);
-val register_proofs = background_theory o Context.theory_map o Thm.register_proofs;
+val register_proofs = background_theory o Thm.register_proofs_thy;
 
 
 (* target contexts *)
diff -r 01041f7bf9b4 -r 2924a83a4a0b src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Aug 31 16:35:30 2012 +0200
+++ b/src/Pure/global_theory.ML	Fri Aug 31 22:24:14 2012 +0200
@@ -124,7 +124,7 @@
 
 (* enter_thms *)
 
-fun register_proofs thms thy = (thms, Context.theory_map (Thm.register_proofs thms) thy);
+fun register_proofs thms thy = (thms, Thm.register_proofs_thy thms thy);
 
 fun enter_thms pre_name post_name app_att (b, thms) thy =
   if Binding.is_empty b
diff -r 01041f7bf9b4 -r 2924a83a4a0b src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Aug 31 16:35:30 2012 +0200
+++ b/src/Pure/more_thm.ML	Fri Aug 31 22:24:14 2012 +0200
@@ -96,6 +96,7 @@
   val kind_rule: string -> thm -> thm
   val kind: string -> attribute
   val register_proofs: thm list -> Context.generic -> Context.generic
+  val register_proofs_thy: thm list -> theory -> theory
   val begin_proofs: Context.generic -> Context.generic
   val join_local_proofs: Proof.context -> unit
   val join_recent_proofs: theory -> unit
@@ -493,6 +494,7 @@
 
 val begin_proofs = Proofs.map (apfst (K empty_proofs));
 val register_proofs = Proofs.map o pairself o add_proofs;
+val register_proofs_thy = Context.theory_map o register_proofs;
 
 val join_local_proofs = force_proofs o #1 o Proofs.get o Context.Proof;
 val join_recent_proofs = force_proofs o #1 o Proofs.get o Context.Theory;