# HG changeset patch # User wenzelm # Date 1292421694 -3600 # Node ID 3f21a269780e2e8a607a5887f0b6a434feec1581 # Parent 2181c47a02fe2523c36345c4234058a5c49162a6 eliminated dead code; diff -r 2181c47a02fe -r 3f21a269780e src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Dec 15 13:35:50 2010 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Dec 15 15:01:34 2010 +0100 @@ -1004,7 +1004,6 @@ (* syntax und parsing *) -structure P = Parse and K = Keyword; val _ = Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl