| changeset 36610 | bafd82950e24 |
| parent 36603 | d5d6111761a6 |
| child 36620 | e6bb250402b5 |
--- a/src/Pure/variable.ML Mon May 03 07:59:51 2010 +0200 +++ b/src/Pure/variable.ML Mon May 03 14:25:56 2010 +0200 @@ -235,7 +235,7 @@ 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 (ProofContext.init (Thm.theory_of_thm th)); +fun global_thm_context th = declare_thm th (ProofContext.init_global (Thm.theory_of_thm th)); (* renaming term/type frees *)