src/Pure/Isar/rule_insts.ML
changeset 30528 7173bf123335
parent 30515 bca05b17b618
child 30545 8209a7196389
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Sun Mar 15 15:59:44 2009 +0100
     1.3 @@ -218,8 +218,8 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
     1.8 -  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
     1.9 +fun where_att x = (Scan.lift (P.and_list inst) >> (fn args =>
    1.10 +  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) x;
    1.11  
    1.12  end;
    1.13  
    1.14 @@ -241,8 +241,8 @@
    1.15  
    1.16  in
    1.17  
    1.18 -val of_att = Attrib.syntax (Scan.lift insts >> (fn args =>
    1.19 -  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)));
    1.20 +fun of_att x = (Scan.lift insts >> (fn args =>
    1.21 +  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
    1.22  
    1.23  end;
    1.24  
    1.25 @@ -250,9 +250,8 @@
    1.26  (* setup *)
    1.27  
    1.28  val _ = Context.>> (Context.map_theory
    1.29 -  (Attrib.add_attributes
    1.30 -   [("where", where_att, "named instantiation of theorem"),
    1.31 -    ("of", of_att, "positional instantiation of theorem")]));
    1.32 + (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
    1.33 +  Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
    1.34  
    1.35  
    1.36