src/Pure/Isar/attrib.ML
changeset 36950 75b8f26f2f07
parent 36787 f60e4dd6d76f
child 36959 f5417836dbea
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat May 15 22:24:25 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat May 15 23:16:32 2010 +0200
     1.3 @@ -48,7 +48,6 @@
     1.4  struct
     1.5  
     1.6  structure T = OuterLex;
     1.7 -structure P = OuterParse;
     1.8  
     1.9  
    1.10  (* source and bindings *)
    1.11 @@ -168,10 +167,10 @@
    1.12  
    1.13  (** parsing attributed theorems **)
    1.14  
    1.15 -val thm_sel = P.$$$ "(" |-- P.list1
    1.16 - (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
    1.17 -  P.nat --| P.minus >> Facts.From ||
    1.18 -  P.nat >> Facts.Single) --| P.$$$ ")";
    1.19 +val thm_sel = Parse.$$$ "(" |-- Parse.list1
    1.20 + (Parse.nat --| Parse.minus -- Parse.nat >> Facts.FromTo ||
    1.21 +  Parse.nat --| Parse.minus >> Facts.From ||
    1.22 +  Parse.nat >> Facts.Single) --| Parse.$$$ ")";
    1.23  
    1.24  local
    1.25  
    1.26 @@ -184,7 +183,7 @@
    1.27      val get_fact = get o Facts.Fact;
    1.28      fun get_named pos name = get (Facts.Named ((name, pos), NONE));
    1.29    in
    1.30 -    P.$$$ "[" |-- Args.attribs (intern thy) --| P.$$$ "]" >> (fn srcs =>
    1.31 +    Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
    1.32        let
    1.33          val atts = map (attribute_i thy) srcs;
    1.34          val (context', th') = Library.apply atts (context, Drule.dummy_thm);
    1.35 @@ -192,7 +191,7 @@
    1.36      ||
    1.37      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    1.38        >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
    1.39 -     Scan.ahead (P.position fact_name) :|-- (fn (name, pos) =>
    1.40 +     Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
    1.41        Args.named_fact (get_named pos) -- Scan.option thm_sel
    1.42          >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
    1.43      -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
    1.44 @@ -223,11 +222,11 @@
    1.45  (* rule composition *)
    1.46  
    1.47  val COMP_att =
    1.48 -  Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
    1.49 +  Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
    1.50      >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)));
    1.51  
    1.52  val THEN_att =
    1.53 -  Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
    1.54 +  Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
    1.55      >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
    1.56  
    1.57  val OF_att =
    1.58 @@ -267,7 +266,7 @@
    1.59  val eta_long =
    1.60    Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
    1.61  
    1.62 -val rotated = Scan.optional P.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
    1.63 +val rotated = Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
    1.64  
    1.65  
    1.66  (* theory setup *)
    1.67 @@ -285,9 +284,9 @@
    1.68      "rename bound variables in abstractions" #>
    1.69    setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
    1.70    setup (Binding.name "folded") folded "folded definitions" #>
    1.71 -  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
    1.72 +  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
    1.73      "number of consumed facts" #>
    1.74 -  setup (Binding.name "constraints") (Scan.lift P.nat >> Rule_Cases.constraints)
    1.75 +  setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
    1.76      "number of equality constraints" #>
    1.77    setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
    1.78      "named rule cases" #>
    1.79 @@ -295,7 +294,7 @@
    1.80      (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
    1.81      "named conclusion of rule cases" #>
    1.82    setup (Binding.name "params")
    1.83 -    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
    1.84 +    (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
    1.85      "named rule parameters" #>
    1.86    setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
    1.87      "result put into standard form (legacy)" #>
    1.88 @@ -345,13 +344,13 @@
    1.89  
    1.90  local
    1.91  
    1.92 -val equals = P.$$$ "=";
    1.93 +val equals = Parse.$$$ "=";
    1.94  
    1.95  fun scan_value (Config.Bool _) =
    1.96        equals -- Args.$$$ "false" >> K (Config.Bool false) ||
    1.97        equals -- Args.$$$ "true" >> K (Config.Bool true) ||
    1.98        Scan.succeed (Config.Bool true)
    1.99 -  | scan_value (Config.Int _) = equals |-- P.int >> Config.Int
   1.100 +  | scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int
   1.101    | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
   1.102  
   1.103  fun scan_config thy config =