src/Pure/Isar/isar_syn.ML
changeset 21033 82f44ceb4fa3
parent 21004 081674431d68
child 21210 c17fd2df4e9e
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Oct 14 23:25:51 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Oct 14 23:25:51 2006 +0200
     1.3 @@ -386,8 +386,11 @@
     1.4    OuterSyntax.command kind ("state " ^ kind) K.thy_goal
     1.5      (P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
     1.6        Scan.ahead (P.locale_keyword || P.statement_keyword)) ("", []) --
     1.7 -      P.general_statement >> (fn ((x, y), (z, w)) =>
     1.8 -      (Toplevel.print o Toplevel.theory_to_proof (Locale.smart_theorem kind x y z w))));
     1.9 +      P.general_statement >> (fn ((loc, a), (elems, concl)) =>
    1.10 +      (Toplevel.print o
    1.11 +       Toplevel.local_theory_to_proof loc
    1.12 +         (Specification.theorem kind NONE (K I) a elems concl) o
    1.13 +       Toplevel.theory_to_proof (Locale.smart_theorem kind loc a elems concl))));
    1.14  
    1.15  val theoremP = gen_theorem PureThy.theoremK;
    1.16  val lemmaP = gen_theorem PureThy.lemmaK;