src/Pure/axclass.ML
changeset 18708 4b3dadb4fe33
parent 18678 dd0c569fa43d
child 18728 6790126ab5f6
     1.1 --- a/src/Pure/axclass.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/Pure/axclass.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -136,7 +136,7 @@
     1.4      in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end;
     1.5  end);
     1.6  
     1.7 -val _ = Context.add_setup [AxclassesData.init];
     1.8 +val _ = Context.add_setup AxclassesData.init;
     1.9  val print_axclasses = AxclassesData.print;
    1.10  
    1.11  
    1.12 @@ -334,10 +334,10 @@
    1.13    HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
    1.14      default_intro_classes_tac facts;
    1.15  
    1.16 -val _ = Context.add_setup [Method.add_methods
    1.17 +val _ = Context.add_setup (Method.add_methods
    1.18   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
    1.19 -   "back-chain introduction rules of axiomatic type classes"),
    1.20 -  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]];
    1.21 +    "back-chain introduction rules of axiomatic type classes"),
    1.22 +  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]);
    1.23  
    1.24  
    1.25