# HG changeset patch # User Christian Urban # Date 1260376261 -3600 # Node ID 178acdd3a64c999702185d7e5ce4c74d91b41256 # Parent ef5b941f00e25fff8890d63f4b3374365ed0f72c fixed minor stupidity diff -r ef5b941f00e2 -r 178acdd3a64c Quot/quotient_def.ML --- a/Quot/quotient_def.ML Wed Dec 09 17:05:33 2009 +0100 +++ b/Quot/quotient_def.ML Wed Dec 09 17:31:01 2009 +0100 @@ -91,7 +91,6 @@ fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm} val lthy'' = Local_Theory.declaration true - val lthy'' = Local_Theory.declaration true (fn phi => let val qconst_str = Binding.name_of qconst_bname