src/Pure/Isar/method.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18824 126049347167
     1.1 --- a/src/Pure/Isar/method.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -581,7 +581,7 @@
     1.4  
     1.5  val add_method = add_methods o Library.single;
     1.6  
     1.7 -fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]);
     1.8 +fun Method name meth cmt = Context.>> (add_method (name, meth, cmt));
     1.9  
    1.10  
    1.11  (* method_setup *)
    1.12 @@ -615,7 +615,7 @@
    1.13  
    1.14  (* sections *)
    1.15  
    1.16 -type modifier = (ProofContext.context -> ProofContext.context) * ProofContext.context attribute;
    1.17 +type modifier = (ProofContext.context -> ProofContext.context) * attribute;
    1.18  
    1.19  local
    1.20  
    1.21 @@ -623,7 +623,7 @@
    1.22  fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
    1.23  fun thmss ss = Scan.repeat (thms ss) >> List.concat;
    1.24  
    1.25 -fun apply (f, att) (ctxt, ths) = Thm.applys_attributes [att] (f ctxt, ths);
    1.26 +fun apply (f, att) (ctxt, ths) = foldl_map (Thm.proof_attributes [att]) (f ctxt, ths);
    1.27  
    1.28  fun section ss = (sect ss -- thmss ss) :-- (fn (m, ths) => Scan.depend (fn ctxt =>
    1.29    Scan.succeed (apply m (ctxt, ths)))) >> #2;
    1.30 @@ -662,13 +662,13 @@
    1.31      >> (pair (I: ProofContext.context -> ProofContext.context) o att);
    1.32  
    1.33  val iprover_modifiers =
    1.34 - [modifier destN Args.bang_colon Args.bang (Attrib.context o ContextRules.dest_bang),
    1.35 -  modifier destN Args.colon (Scan.succeed ()) (Attrib.context o ContextRules.dest),
    1.36 -  modifier elimN Args.bang_colon Args.bang (Attrib.context o ContextRules.elim_bang),
    1.37 -  modifier elimN Args.colon (Scan.succeed ()) (Attrib.context o ContextRules.elim),
    1.38 -  modifier introN Args.bang_colon Args.bang (Attrib.context o ContextRules.intro_bang),
    1.39 -  modifier introN Args.colon (Scan.succeed ()) (Attrib.context o ContextRules.intro),
    1.40 -  Args.del -- Args.colon >> K (I, Attrib.context ContextRules.rule_del)];
    1.41 + [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
    1.42 +  modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
    1.43 +  modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
    1.44 +  modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
    1.45 +  modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
    1.46 +  modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
    1.47 +  Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
    1.48  
    1.49  in
    1.50