# HG changeset patch
# User wenzelm
# Date 1185559909 -7200
# Node ID 60ac90b795be9f98b6b5420a330e51e5b713cd5d
# Parent  2d473ed154914763cc3096e19aa812fcfe2afc6d
Druke.dummy_thm;

diff -r 2d473ed15491 -r 60ac90b795be src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Jul 27 20:11:48 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Jul 27 20:11:49 2007 +0200
@@ -1657,14 +1657,14 @@
 
 local
 
-val dummy_thm = Drule.mk_term (Thm.cterm_of ProtoPure.thy (Term.dummy_pattern propT));
 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
 
 fun add_decls add loc decl =
   ProofContext.theory (change_locale loc
     (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
       (axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
-  add_thmss loc Thm.internalK [(("", [Attrib.internal (decl_attrib decl)]), [([dummy_thm], [])])];
+  add_thmss loc Thm.internalK
+    [(("", [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
 
 in