Specification.theorem now also takes "interactive" flag as argument.
authorberghofe
Tue Aug 28 18:01:37 2007 +0200 (2007-08-28 ago)
changeset 244517c205d006719
parent 24450 70fd99d4ef82
child 24452 93b113c5ac33
Specification.theorem now also takes "interactive" flag as argument.
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Aug 28 16:33:52 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 28 18:01:37 2007 +0200
     1.3 @@ -455,7 +455,7 @@
     1.4        Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
     1.5        SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
     1.6        (Toplevel.print o
     1.7 -       Toplevel.local_theory_to_proof loc
     1.8 +       Toplevel.local_theory_to_proof' loc
     1.9           (Specification.theorem kind NONE (K I) a elems concl))));
    1.10  
    1.11  val theoremP = gen_theorem Thm.theoremK;