Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Druke.dummy_thm;
authorwenzelm
Fri, 27 Jul 2007 20:11:49 +0200
changeset 24006 60ac90b795be
parent 24005 2d473ed15491
child 24007 8f40e6fdb376
Druke.dummy_thm;
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle