src/Pure/simplifier.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18988 d6e5fa2ba8b8
     1.1 --- a/src/Pure/simplifier.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -64,11 +64,11 @@
     1.4    val print_local_simpset: Proof.context -> unit
     1.5    val get_local_simpset: Proof.context -> simpset
     1.6    val put_local_simpset: simpset -> Proof.context -> Proof.context
     1.7 -  val attrib: (simpset * thm list -> simpset) -> Context.generic attribute
     1.8 -  val simp_add: Context.generic attribute
     1.9 -  val simp_del: Context.generic attribute
    1.10 -  val cong_add: Context.generic attribute
    1.11 -  val cong_del: Context.generic attribute
    1.12 +  val attrib: (simpset * thm list -> simpset) -> attribute
    1.13 +  val simp_add: attribute
    1.14 +  val simp_del: attribute
    1.15 +  val cong_add: attribute
    1.16 +  val cong_del: attribute
    1.17    val cong_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    1.18    val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
    1.19    val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    1.20 @@ -138,7 +138,7 @@
    1.21  
    1.22  (* attributes *)
    1.23  
    1.24 -fun attrib f = Attrib.declaration (fn th =>
    1.25 +fun attrib f = Thm.declaration_attribute (fn th =>
    1.26     fn Context.Theory thy => (change_simpset_of thy (fn ss => f (ss, [th])); Context.Theory thy)
    1.27      | Context.Proof ctxt => Context.Proof (LocalSimpset.map (fn ss => f (ss, [th])) ctxt));
    1.28  
    1.29 @@ -251,7 +251,7 @@
    1.30  in
    1.31  
    1.32  val simplified =
    1.33 -  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Attrib.rule (fn x =>
    1.34 +  Attrib.syntax (conv_mode -- Attrib.thmss >> (fn (f, ths) => Thm.rule_attribute (fn x =>
    1.35      f ((if null ths then I else MetaSimplifier.clear_ss) (get_ss x) addsimps ths))));
    1.36  
    1.37  end;
    1.38 @@ -261,11 +261,9 @@
    1.39  
    1.40  val _ = Context.add_setup
    1.41   (Attrib.add_attributes
    1.42 -   [(simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
    1.43 -      "declaration of Simplifier rule"),
    1.44 -    (congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
    1.45 -      "declaration of Simplifier congruence rule"),
    1.46 -    ("simplified", Attrib.common simplified, "simplified rule")]);
    1.47 +   [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rule"),
    1.48 +    (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
    1.49 +    ("simplified", simplified, "simplified rule")]);
    1.50  
    1.51  
    1.52  
    1.53 @@ -286,23 +284,23 @@
    1.54    >> (curry (Library.foldl op o) I o rev)) x;
    1.55  
    1.56  val cong_modifiers =
    1.57 - [Args.$$$ congN -- Args.colon >> K ((I, Attrib.context cong_add): Method.modifier),
    1.58 -  Args.$$$ congN -- Args.add -- Args.colon >> K (I, Attrib.context cong_add),
    1.59 -  Args.$$$ congN -- Args.del -- Args.colon >> K (I, Attrib.context cong_del)];
    1.60 + [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
    1.61 +  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
    1.62 +  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
    1.63  
    1.64  val simp_modifiers =
    1.65 - [Args.$$$ simpN -- Args.colon >> K (I, Attrib.context simp_add),
    1.66 -  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, Attrib.context simp_add),
    1.67 -  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, Attrib.context simp_del),
    1.68 + [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
    1.69 +  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
    1.70 +  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
    1.71    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
    1.72 -    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
    1.73 +    >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
    1.74     @ cong_modifiers;
    1.75  
    1.76  val simp_modifiers' =
    1.77 - [Args.add -- Args.colon >> K (I, Attrib.context simp_add),
    1.78 -  Args.del -- Args.colon >> K (I, Attrib.context simp_del),
    1.79 + [Args.add -- Args.colon >> K (I, simp_add),
    1.80 +  Args.del -- Args.colon >> K (I, simp_del),
    1.81    Args.$$$ onlyN -- Args.colon
    1.82 -    >> K (LocalSimpset.map MetaSimplifier.clear_ss, Attrib.context simp_add)]
    1.83 +    >> K (LocalSimpset.map MetaSimplifier.clear_ss, simp_add)]
    1.84     @ cong_modifiers;
    1.85  
    1.86  fun simp_args more_mods =