src/Pure/Isar/method.ML
changeset 18708 4b3dadb4fe33
parent 18640 61627ae3ddc3
child 18728 6790126ab5f6
     1.1 --- a/src/Pure/Isar/method.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -544,7 +544,7 @@
     1.4      end;
     1.5  end);
     1.6  
     1.7 -val _ = Context.add_setup [MethodsData.init];
     1.8 +val _ = Context.add_setup MethodsData.init;
     1.9  val print_methods = MethodsData.print;
    1.10  
    1.11  
    1.12 @@ -721,9 +721,9 @@
    1.13  val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac;
    1.14  
    1.15  
    1.16 -(* pure_methods *)
    1.17 +(* theory setup *)
    1.18  
    1.19 -val pure_methods =
    1.20 +val _ = Context.add_setup (add_methods
    1.21   [("fail", no_args fail, "force failure"),
    1.22    ("succeed", no_args succeed, "succeed"),
    1.23    ("-", no_args insert_facts, "do nothing (insert current facts only)"),
    1.24 @@ -751,9 +751,7 @@
    1.25    ("thin_tac", thin_meth, "remove premise (dynamic instantiation)"),
    1.26    ("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"),
    1.27    ("rotate_tac", rotate_meth, "rotate assumptions of goal"),
    1.28 -  ("tactic", simple_args Args.name tactic, "ML tactic as proof method")];
    1.29 -
    1.30 -val _ = Context.add_setup [add_methods pure_methods];
    1.31 +  ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);
    1.32  
    1.33  
    1.34  (*final declarations of this structure!*)