src/Pure/Isar/rule_insts.ML
changeset 36950 75b8f26f2f07
parent 33368 b1cf34f1855c
child 36959 f5417836dbea
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Sat May 15 22:24:25 2010 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat May 15 23:16:32 2010 +0200
     1.3 @@ -30,7 +30,6 @@
     1.4  struct
     1.5  
     1.6  structure T = OuterLex;
     1.7 -structure P = OuterParse;
     1.8  
     1.9  
    1.10  (** reading instantiations **)
    1.11 @@ -215,14 +214,14 @@
    1.12    Args.internal_term >> T.Term ||
    1.13    Args.name_source >> T.Text;
    1.14  
    1.15 -val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
    1.16 +val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead Parse.not_eof -- value)
    1.17    >> (fn (xi, (a, v)) => (a, (xi, v)));
    1.18  
    1.19  in
    1.20  
    1.21  val _ = Context.>> (Context.map_theory
    1.22    (Attrib.setup (Binding.name "where")
    1.23 -    (Scan.lift (P.and_list inst) >> (fn args =>
    1.24 +    (Scan.lift (Parse.and_list inst) >> (fn args =>
    1.25        Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
    1.26      "named instantiation of theorem"));
    1.27  
    1.28 @@ -237,7 +236,7 @@
    1.29    Args.internal_term >> T.Term ||
    1.30    Args.name_source >> T.Text;
    1.31  
    1.32 -val inst = Scan.ahead P.not_eof -- Args.maybe value;
    1.33 +val inst = Scan.ahead Parse.not_eof -- Args.maybe value;
    1.34  val concl = Args.$$$ "concl" -- Args.colon;
    1.35  
    1.36  val insts =
    1.37 @@ -387,7 +386,8 @@
    1.38  fun method inst_tac tac =
    1.39    Args.goal_spec --
    1.40    Scan.optional (Scan.lift
    1.41 -    (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
    1.42 +    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
    1.43 +      Args.$$$ "in")) [] --
    1.44    Attrib.thms >>
    1.45    (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
    1.46      if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
    1.47 @@ -425,5 +425,5 @@
    1.48  
    1.49  end;
    1.50  
    1.51 -structure BasicRuleInsts: BASIC_RULE_INSTS = RuleInsts;
    1.52 -open BasicRuleInsts;
    1.53 +structure Basic_Rule_Insts: BASIC_RULE_INSTS = RuleInsts;
    1.54 +open Basic_Rule_Insts;