src/Pure/Isar/isar_syn.ML
changeset 22351 587845efb4cf
parent 22340 275802767bf3
child 22385 cc2be3315e72
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Feb 23 08:39:23 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 23 08:39:24 2007 +0100
     1.3 @@ -378,12 +378,12 @@
     1.4  
     1.5  val localeP =
     1.6    OuterSyntax.command "locale" "define named proof context" K.thy_decl
     1.7 -    ((P.opt_keyword "open" >> not) -- P.name
     1.8 +    ((P.opt_keyword "open" >> (fn true => NONE | false => SOME "")) -- P.name
     1.9          -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
    1.10          -- P.opt_begin
    1.11        >> (fn (((is_open, name), (expr, elems)), begin) =>
    1.12            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
    1.13 -            (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin false)));
    1.14 +            (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin)));
    1.15  
    1.16  val interpretationP =
    1.17    OuterSyntax.command "interpretation"
    1.18 @@ -391,14 +391,14 @@
    1.19      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
    1.20        >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
    1.21        SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts >> (fn ((x, y), z) =>
    1.22 -        Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I x y z)));
    1.23 +        Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
    1.24  
    1.25  val interpretP =
    1.26    OuterSyntax.command "interpret"
    1.27      "prove and register interpretation of locale expression in proof context"
    1.28      (K.tag_proof K.prf_goal)
    1.29      (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
    1.30 -      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z)));
    1.31 +      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
    1.32  
    1.33  
    1.34  (* classes *)
    1.35 @@ -420,7 +420,7 @@
    1.36      -- P.opt_begin
    1.37      >> (fn ((bname, (supclasses, elems)), begin) =>
    1.38          Toplevel.begin_local_theory begin
    1.39 -          (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin true)));
    1.40 +          (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin)));
    1.41  
    1.42  val instanceP =
    1.43    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((