src/Pure/Isar/rule_insts.ML
changeset 30722 623d4831c8cf
parent 30551 24e156db414c
child 30763 6976521b4263
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Mar 25 21:35:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Mar 26 14:14:02 2009 +0100
     1.3 @@ -220,8 +220,11 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun where_att x = (Scan.lift (P.and_list inst) >> (fn args =>
     1.8 -  Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) x;
     1.9 +val _ = Context.>> (Context.map_theory
    1.10 +  (Attrib.setup (Binding.name "where")
    1.11 +    (Scan.lift (P.and_list inst) >> (fn args =>
    1.12 +      Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
    1.13 +    "named instantiation of theorem"));
    1.14  
    1.15  end;
    1.16  
    1.17 @@ -243,19 +246,15 @@
    1.18  
    1.19  in
    1.20  
    1.21 -fun of_att x = (Scan.lift insts >> (fn args =>
    1.22 -  Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
    1.23 +val _ = Context.>> (Context.map_theory
    1.24 +  (Attrib.setup (Binding.name "of")
    1.25 +    (Scan.lift insts >> (fn args =>
    1.26 +      Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
    1.27 +    "positional instantiation of theorem"));
    1.28  
    1.29  end;
    1.30  
    1.31  
    1.32 -(* setup *)
    1.33 -
    1.34 -val _ = Context.>> (Context.map_theory
    1.35 - (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
    1.36 -  Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
    1.37 -
    1.38 -
    1.39  
    1.40  (** tactics **)
    1.41