--- a/src/Pure/variable.ML Sun Dec 21 19:14:16 2014 +0100
+++ b/src/Pure/variable.ML Sun Dec 21 22:49:17 2014 +0100
@@ -25,7 +25,6 @@
val declare_typ: typ -> Proof.context -> Proof.context
val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
val declare_thm: thm -> Proof.context -> Proof.context
- val global_thm_context: thm -> Proof.context
val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
val bind_term: indexname * term option -> Proof.context -> Proof.context
val expand_binds: Proof.context -> term -> term
@@ -269,7 +268,6 @@
val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
val declare_thm = Thm.fold_terms declare_internal;
-fun global_thm_context th = declare_thm th (Proof_Context.init_global (Thm.theory_of_thm th));
(* renaming term/type frees *)