# HG changeset patch # User wenzelm # Date 1162924788 -3600 # Node ID 54faccb5d6f6371f60ce089c813dd5b36f1a130e # Parent 76d6d445d69b7346ff00bbb08e9f2e3f3d9cf549 removed obsolete Locale.smart_theorem; diff -r 76d6d445d69b -r 54faccb5d6f6 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Nov 07 19:39:46 2006 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue Nov 07 19:39:48 2006 +0100 @@ -389,8 +389,7 @@ P.general_statement >> (fn ((loc, a), (elems, concl)) => (Toplevel.print o Toplevel.local_theory_to_proof loc - (Specification.theorem kind NONE (K I) a elems concl) o - Toplevel.theory_to_proof (Locale.smart_theorem kind loc a elems concl)))); + (Specification.theorem kind NONE (K I) a elems concl)))); val theoremP = gen_theorem PureThy.theoremK; val lemmaP = gen_theorem PureThy.lemmaK;