src/Pure/Isar/rule_insts.ML
changeset 26463 9283b4185fdf
parent 26435 bdce320cd426
child 27120 b21eec437295
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Fri Mar 28 19:43:54 2008 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Fri Mar 28 20:02:04 2008 +0100
     1.3 @@ -218,9 +218,10 @@
     1.4  
     1.5  (* setup *)
     1.6  
     1.7 -val _ = Context.>> (Attrib.add_attributes
     1.8 - [("where", where_att, "named instantiation of theorem"),
     1.9 -  ("of", of_att, "positional instantiation of theorem")]);
    1.10 +val _ = Context.>> (Context.map_theory
    1.11 +  (Attrib.add_attributes
    1.12 +   [("where", where_att, "named instantiation of theorem"),
    1.13 +    ("of", of_att, "positional instantiation of theorem")]));
    1.14  
    1.15  
    1.16  
    1.17 @@ -367,21 +368,22 @@
    1.18  
    1.19  (* setup *)
    1.20  
    1.21 -val _ = Context.>> (Method.add_methods
    1.22 - [("rule_tac", inst_args_var res_inst_meth,
    1.23 -    "apply rule (dynamic instantiation)"),
    1.24 -  ("erule_tac", inst_args_var eres_inst_meth,
    1.25 -    "apply rule in elimination manner (dynamic instantiation)"),
    1.26 -  ("drule_tac", inst_args_var dres_inst_meth,
    1.27 -    "apply rule in destruct manner (dynamic instantiation)"),
    1.28 -  ("frule_tac", inst_args_var forw_inst_meth,
    1.29 -    "apply rule in forward manner (dynamic instantiation)"),
    1.30 -  ("cut_tac", inst_args_var cut_inst_meth,
    1.31 -    "cut rule (dynamic instantiation)"),
    1.32 -  ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
    1.33 -    "insert subgoal (dynamic instantiation)"),
    1.34 -  ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
    1.35 -    "remove premise (dynamic instantiation)")]);
    1.36 +val _ = Context.>> (Context.map_theory
    1.37 +  (Method.add_methods
    1.38 +   [("rule_tac", inst_args_var res_inst_meth,
    1.39 +      "apply rule (dynamic instantiation)"),
    1.40 +    ("erule_tac", inst_args_var eres_inst_meth,
    1.41 +      "apply rule in elimination manner (dynamic instantiation)"),
    1.42 +    ("drule_tac", inst_args_var dres_inst_meth,
    1.43 +      "apply rule in destruct manner (dynamic instantiation)"),
    1.44 +    ("frule_tac", inst_args_var forw_inst_meth,
    1.45 +      "apply rule in forward manner (dynamic instantiation)"),
    1.46 +    ("cut_tac", inst_args_var cut_inst_meth,
    1.47 +      "cut rule (dynamic instantiation)"),
    1.48 +    ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
    1.49 +      "insert subgoal (dynamic instantiation)"),
    1.50 +    ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
    1.51 +      "remove premise (dynamic instantiation)")]));
    1.52  
    1.53  end;
    1.54