src/Pure/Isar/rule_insts.ML
changeset 27882 eaa9fef9f4c1
parent 27809 a1e409db516b
child 28083 103d9282a946
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Aug 14 21:06:07 2008 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Fri Aug 15 15:50:44 2008 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4  val value =
     1.5    Args.internal_typ >> T.Typ ||
     1.6    Args.internal_term >> T.Term ||
     1.7 -  Args.name >> T.Text;
     1.8 +  Args.name_source >> T.Text;
     1.9  
    1.10  val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
    1.11    >> (fn (xi, (a, v)) => (a, (xi, v)));
    1.12 @@ -231,7 +231,7 @@
    1.13  
    1.14  val value =
    1.15    Args.internal_term >> T.Term ||
    1.16 -  Args.name >> T.Text;
    1.17 +  Args.name_source >> T.Text;
    1.18  
    1.19  val inst = Scan.ahead P.not_eof -- Args.maybe value;
    1.20  val concl = Args.$$$ "concl" -- Args.colon;
    1.21 @@ -408,16 +408,16 @@
    1.22  (* method syntax *)
    1.23  
    1.24  val insts =
    1.25 -  Scan.optional
    1.26 -    (Scan.lift (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
    1.27 +  Scan.optional (Scan.lift
    1.28 +    (P.and_list1 (Args.name -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
    1.29      -- Attrib.thms;
    1.30  
    1.31  fun inst_args f src ctxt =
    1.32    f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
    1.33  
    1.34  val insts_var =
    1.35 -  Scan.optional
    1.36 -    (Scan.lift (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name)) --| Args.$$$ "in")) []
    1.37 +  Scan.optional (Scan.lift
    1.38 +    (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) []
    1.39      -- Attrib.thms;
    1.40  
    1.41  fun inst_args_var f src ctxt =
    1.42 @@ -438,13 +438,12 @@
    1.43        "apply rule in forward manner (dynamic instantiation)"),
    1.44      ("cut_tac", inst_args_var cut_inst_meth,
    1.45        "cut rule (dynamic instantiation)"),
    1.46 -    ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
    1.47 +    ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name_source) subgoals_tac,
    1.48        "insert subgoal (dynamic instantiation)"),
    1.49 -    ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
    1.50 +    ("thin_tac", Method.goal_args_ctxt Args.name_source thin_tac,
    1.51        "remove premise (dynamic instantiation)")]));
    1.52  
    1.53  end;
    1.54  
    1.55  structure BasicRuleInsts: BASIC_RULE_INSTS = RuleInsts;
    1.56  open BasicRuleInsts;
    1.57 -