src/Pure/Isar/isar_syn.ML
changeset 21228 54faccb5d6f6
parent 21210 c17fd2df4e9e
child 21269 c605503bb4ef
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 07 19:39:46 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 07 19:39:48 2006 +0100
     1.3 @@ -389,8 +389,7 @@
     1.4        P.general_statement >> (fn ((loc, a), (elems, concl)) =>
     1.5        (Toplevel.print o
     1.6         Toplevel.local_theory_to_proof loc
     1.7 -         (Specification.theorem kind NONE (K I) a elems concl) o
     1.8 -       Toplevel.theory_to_proof (Locale.smart_theorem kind loc a elems concl))));
     1.9 +         (Specification.theorem kind NONE (K I) a elems concl))));
    1.10  
    1.11  val theoremP = gen_theorem PureThy.theoremK;
    1.12  val lemmaP = gen_theorem PureThy.lemmaK;