src/Pure/proof_general.ML
changeset 16958 1b4a3110c64a
parent 16896 db2defb39f4c
child 17018 1e9e0f5877f2
     1.1 --- a/src/Pure/proof_general.ML	Fri Jul 29 15:20:29 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Fri Jul 29 16:16:44 2005 +0200
     1.3 @@ -858,7 +858,7 @@
     1.4              val thmnameP = (* see isar_syn.ML/theoremsP *)
     1.5                  let
     1.6                      val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
     1.7 -                    val theoremsP = P.locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
     1.8 +                    val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
     1.9                  in
    1.10                      theoremsP
    1.11                  end
    1.12 @@ -896,12 +896,12 @@
    1.13              statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
    1.14  
    1.15              val gen_theoremP =
    1.16 -                P.locale_target -- Scan.optional (P.opt_thm_name ":" --|
    1.17 +                P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
    1.18                   Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
    1.19                                   general_statement >> (fn ((locale, a), (elems, concl)) =>
    1.20                                                           fst a) (* a : (bstring * Args.src list) *)
    1.21  
    1.22 -            val nameP = P.locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
    1.23 +            val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
    1.24              (* TODO: add preference values for attributes
    1.25                 val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
    1.26              *)